Fix imports in Coq modules

3 files changed, 35 insertions, 26 deletions

diff --git a/src/common/IntegerExtra.v b/src/common/IntegerExtra.v
index d36fcee..2b6cded 100644
--- a/src/common/IntegerExtra.v
+++ b/src/common/IntegerExtra.v
@@ -17,13 +17,14 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-Require Import BinInt.
-Require Import Lia.
-Require Import ZBinary.
+Require Import Coq.ZArith.BinInt.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Numbers.Integer.Binary.ZBinary.
 
-From compcert Require Import Integers Coqlib.
+Require Import compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
 
-Require Import Vericertlib.
+Require Import vericert.common.Vericertlib.
 
 Local Open Scope Z_scope.
 
@@ -337,7 +338,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr Byte.zwordsize)) i). rewrite bits_shru.
     change (unsigned (repr Byte.zwordsize)) with Byte.zwordsize.
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_byte3:
@@ -347,7 +348,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (2 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (2 * Byte.zwordsize))) with (2 * Byte.zwordsize).
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_byte4:
@@ -357,7 +358,7 @@ Module IntExtra.
     assert (zwordsize = 4 * Byte.zwordsize) by reflexivity.
     fold (testbit (shru n (repr (3 * Byte.zwordsize))) i). rewrite bits_shru.
     change (unsigned (repr (3 * Byte.zwordsize))) with (3 * Byte.zwordsize).
-    apply zlt_true. omega. omega.
+    apply zlt_true. lia. lia.
   Qed.
 
   Lemma bits_ofwords:
diff --git a/src/common/Maps.v b/src/common/Maps.v
index 696c9b8..f0f264d 100644
--- a/src/common/Maps.v
+++ b/src/common/Maps.v
@@ -17,13 +17,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From vericert Require Import Vericertlib.
+Set Implicit Arguments.
 
-From compcert Require Export Maps.
-From compcert Require Import Errors.
-Import PTree.
+Require Export compcert.lib.Maps.
 
-Set Implicit Arguments.
+Require Import compcert.common.Errors.
+
+Require Import vericert.common.Vericertlib.
+
+Import PTree.
 
 Local Open Scope error_monad_scope.
 
diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v
index d9176db..4f6c6fa 100644
--- a/src/common/Vericertlib.v
+++ b/src/common/Vericertlib.v
@@ -1,6 +1,7 @@
 (*
  * Vericert: Verified high-level synthesis.
- * Copyright (C) 2019-2020 Yann Herklotz <yann@yannherklotz.com>
+ * Copyright (C) 2019-2021 Yann Herklotz <yann@yannherklotz.com>
+ *               2020 James Pollard <j@mes.dev>
  *
  * This program is free software: you can redistribute it and/or modify
  * it under the terms of the GNU General Public License as published by
@@ -16,21 +17,23 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From Coq Require Export
-     String
-     ZArith
-     Znumtheory
-     List
-     Bool.
+Set Implicit Arguments.
 
-Require Import Lia.
+Require Export Coq.Bool.Bool.
+Require Export Coq.Lists.List.
+Require Export Coq.Strings.String.
+Require Export Coq.ZArith.ZArith.
+Require Export Coq.ZArith.Znumtheory.
+Require Import Coq.micromega.Lia.
 
-From vericert Require Import Show.
+Require Export compcert.lib.Coqlib.
+Require Import compcert.lib.Integers.
+
+Require Export vericert.common.VericertTactics.
+Require Import vericert.common.Show.
 
 (* Depend on CompCert for the basic library, as they declare and prove some
    useful theorems. *)
-From compcert.lib Require Export Coqlib.
-From compcert Require Import Integers.
 
 Local Open Scope Z_scope.
 
@@ -70,7 +73,9 @@ Ltac solve_by_invert := solve_by_inverts 1.
 Ltac invert x := inversion x; subst; clear x.
 
 Ltac destruct_match :=
-  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end.
+  match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? end.
+
+Ltac auto_destruct x := destruct_with_eqn x; simpl in *; try discriminate; try congruence.
 
 Ltac nicify_hypotheses :=
   repeat match goal with
@@ -180,7 +185,8 @@ Ltac liapp :=
          | _ => idtac
          end.
 
-Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption.
+Ltac crush := simplify; try discriminate; try congruence; try lia; liapp;
+              try assumption; try (solve [auto]).
 
 Global Opaque Nat.div.
 Global Opaque Z.mul.