From 7de50f87b68fcc83bb13f1478a1fbad9bea8c866 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 7 Oct 2016 13:20:53 +0200
Subject: [PATCH] Avoid camelcased names.

---
 algebra/upred.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 096ca4dd2..d3ddbbcd8 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -1492,11 +1492,11 @@ Proof.
   eapply IH with x'; eauto using cmra_validN_S, cmra_validN_op_l.
 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.
 
 Corollary consistency : ¬ (True ⊢ False).
-Proof. exact (consistencyModal 0). Qed.
+Proof. exact (consistency_modal 0). Qed.
 End uPred_logic.
 
 (* Hint DB for the logic *)
-- 
GitLab