Commit cd511950 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix indentation.

parent db5bd60a
......@@ -190,7 +190,7 @@ Global Instance from_forall_later {A} P (Φ : A → PROP) name :
Proof. rewrite /FromForall=> <-. by rewrite later_forall. Qed.
Global Instance from_forall_laterN {A} P (Φ : A PROP) n name :
FromForall P Φ name FromForall (^n P) (λ a, ^n (Φ a))%I name.
FromForall P Φ name FromForall (^n P) (λ a, ^n (Φ a))%I name.
Proof. rewrite /FromForall => <-. by rewrite laterN_forall. Qed.
Global Instance from_forall_except_0 {A} P (Φ : A PROP) name :
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment