Fix indent

huynhtrankhanh · Nov 14, 2023 · d0e33a5 · d0e33a5
1 parent 2b6813e
commit d0e33a5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Imperative.v b/theories/Imperative.v
@@ -21,7 +21,7 @@ Proof.
   - case b as [| effect2 continuation2].
     + exact False.
     + pose proof (ltac:(intro hEffect; subst effect; exact (forall response, identical _ _ _ (continuation response) (continuation2 response))) : effect = effect2 -> Prop) as rhs.
-    exact (effect = effect2 /\ forall x: effect = effect2, rhs x).
+      exact (effect = effect2 /\ forall x: effect = effect2, rhs x).
 Defined.
 
 Fixpoint bind {effectType effectResponse A B} (a : Action effectType effectResponse A) (f : A -> Action effectType effectResponse B) : Action effectType effectResponse B :=