Update Coq version to 8.14.1

3 files changed, 12 insertions, 39 deletions

diff --git a/src/common/Maps.v b/src/common/Maps.v
index f0f264d..13ca276 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -17,7 +17,7 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Set Implicit Arguments.
+(*Set Implicit Arguments.
 
 Require Export compcert.lib.Maps.
 
@@ -62,3 +62,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m
 Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f).
 
 End PTree.
+*)
diff --git a/src/common/Show.v b/src/common/Show.v
index 4c66725..20c07e7 100644
--- a/src/common/Show.v
+++ b/src/common/Show.v
@@ -1,4 +1,4 @@
-(* 
+(*
  * Vericert: Verified high-level synthesis.
  * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
  *
@@ -24,15 +24,11 @@ From Coq Require Import
 
 Local Open Scope string.
 
-Class Show A : Type :=
-  {
-  show : A -> string
-  }.
+Class Show A : Type := { show : A -> string }.
 
+#[export]
 Instance showBool : Show bool :=
-  {
-  show := fun b:bool => if b then "true" else "false"
-  }.
+  { show := fun b:bool => if b then "true" else "false" }.
 
 Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
   let d := match n mod 10 with
@@ -52,17 +48,11 @@ Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string :=
 Definition string_of_nat (n : nat) : string :=
   string_of_nat_aux n n "".
 
-Instance showNat : Show nat :=
-  {
-  show := string_of_nat
-  }.
+#[export]
+Instance showNat : Show nat := { show := string_of_nat }.
 
-Instance showZ : Show Z :=
-  {
-  show a := show (Z.to_nat a)
-  }.
+#[export]
+Instance showZ : Show Z := { show a := show (Z.to_nat a) }.
 
-Instance showPositive : Show positive :=
-  {
-  show a := show (Zpos a)
-  }.
+#[export]
+Instance showPositive : Show positive := { show a := show (Zpos a) }.
diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v
index 62ca54d..3a27cc6 100644
--- a/src/common/ZExtra.v
+++ b/src/common/ZExtra.v
@@ -45,12 +45,6 @@ Proof.
   - apply Z.mod_divide; assumption.
 Qed.
 
-Lemma mod_0_r: forall (m: Z),
-    m mod 0 = 0.
-Proof.
-  intros. destruct m; reflexivity.
-Qed.
-
 Lemma sub_mod_0: forall (a b m: Z),
     a mod m = 0 ->
     b mod m = 0 ->
@@ -89,18 +83,6 @@ Proof.
   reflexivity.
 Qed.
 
-Lemma mod_pow2_same_cases: forall a n,
-    a mod 2 ^ n = a ->
-    2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n.
-Proof.
-  intros.
-  assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C].
-  - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto.
-  - right.
-    rewrite <- H. apply Z.mod_pos_bound.
-    apply Z.pow_pos_nonneg; lia.
-Qed.
-
 Lemma mod_pow2_same_bounds: forall a n,
     a mod 2 ^ n = a ->
     0 <= n ->