Skip to content
Snippets Groups Projects
Commit 7de50f87 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Avoid camelcased names.

parent e5c563f9
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
algebra/upred.v
+ 2
− 2
View file @ 7de50f87
...@@ -1492,11 +1492,11 @@ Proof. ...@@ -1492,11 +1492,11 @@ Proof.
eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l. eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
Qed. Qed.
Corollary consistencyModal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False). Corollary consistency_modal n : ¬ (True ⊢ Nat.iter n (λ P, |=r=> ▷ P) False).
Proof. exact (adequacy False n). Qed. Proof. exact (adequacy False n). Qed.
Corollary consistency : ¬ (True ⊢ False). Corollary consistency : ¬ (True ⊢ False).
Proof. exact (consistencyModal 0). Qed. Proof. exact (consistency_modal 0). Qed.
End uPred_logic. End uPred_logic.
(* Hint DB for the logic *) (* Hint DB for the logic *)
......
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