From ac26c5e6bfd5e04052bf04bf8d61b86dfd996da9 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Mon, 15 Apr 2024 18:52:09 +0000 Subject: [PATCH] Require Vector directly instead of through Bvector --- doc/equations_intro.v | 4 ++-- examples/Basics.v | 4 ++-- test-suite/Basics.v | 4 ++-- test-suite/BasicsDec.v | 3 ++- test-suite/Below.v | 2 +- test-suite/f91.v | 2 +- test-suite/issues/issue43.v | 3 ++- test-suite/noconf_hom.v | 3 ++- test-suite/nolam.v | 2 +- test-suite/rec.v | 2 +- theories/Prop/NoConfusion.v | 2 +- 11 files changed, 17 insertions(+), 14 deletions(-) diff --git a/doc/equations_intro.v b/doc/equations_intro.v index d1749a38c..8d0de9e1e 100644 --- a/doc/equations_intro.v +++ b/doc/equations_intro.v @@ -16,7 +16,7 @@ From Equations Require Import Equations. (* begin hide *) Check @eq. -Require Import Bvector. +Require Import Vector. (* Derive DependentElimination for nat bool option sum Datatypes.prod list *) (* end hide *) @@ -573,4 +573,4 @@ End KAxiom. the graph and elimination principle for the function, and the propositional equalities of the definition. Note that `eliminator=yes` forces `equations=yes`. -*) \ No newline at end of file +*) diff --git a/examples/Basics.v b/examples/Basics.v index 1babe7ada..56b29f806 100644 --- a/examples/Basics.v +++ b/examples/Basics.v @@ -22,7 +22,7 @@ If running this interactively you can ignore the printing and hide directives which are just used to instruct coqdoc. *) -Require Import Program Bvector List Relations. +Require Import Program List Relations. From Equations Require Import Equations Signature. Require Import Utf8. @@ -336,7 +336,7 @@ Qed. (* Eval compute in @zip''. *) -Require Import Bvector. +Require Vector. (** This function can also be defined by structural recursion on [m]. *) diff --git a/test-suite/Basics.v b/test-suite/Basics.v index e86ba5665..13aee33ff 100644 --- a/test-suite/Basics.v +++ b/test-suite/Basics.v @@ -6,7 +6,7 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Program Bvector List Relations. +Require Import Program Vector List Relations. Require Import Equations.Prop.Equations. Require Import Utf8. Set Keyed Unification. @@ -435,7 +435,7 @@ Extraction split. *) (* Eval compute in @zip''. *) -Require Import Bvector. +Require Vector. Import VectorNotations. Equations split_struct {X : Type} {m n} (xs : vector X (m + n)) : Split m n xs := split_struct (m:=0) xs := append nil xs ; diff --git a/test-suite/BasicsDec.v b/test-suite/BasicsDec.v index 7585aaa98..e96a685e6 100644 --- a/test-suite/BasicsDec.v +++ b/test-suite/BasicsDec.v @@ -1,4 +1,5 @@ -Require Import Equations.Prop.Equations Bvector. +Require Vector. +Require Import Equations.Prop.Equations. Inductive bar1 (A : Type) : A -> Prop := . Inductive bar2 (A : Type) : (A -> A) -> Prop := . diff --git a/test-suite/Below.v b/test-suite/Below.v index f701763b2..a7e453ede 100644 --- a/test-suite/Below.v +++ b/test-suite/Below.v @@ -9,7 +9,6 @@ (** Instances of [Below] for the standard datatypes. To be used by [equations] when it needs to do recursion on a type. *) -Require Import Bvector. Require Import Vectors.Vector. Require Import Equations.Init Equations.CoreTactics Equations.Prop.DepElim Equations.Prop.Tactics Equations.Prop.Constants. @@ -87,6 +86,7 @@ Arguments cons {A} _ {n}. Open Scope equations_scope. +Import VectorNotations. Import EquationsNotations. Equations Below_vector A (P : forall n, vector A n -> Type) n (v : vector A n) : Type diff --git a/test-suite/f91.v b/test-suite/f91.v index ba4f0d5c6..5fbd27a91 100644 --- a/test-suite/f91.v +++ b/test-suite/f91.v @@ -7,7 +7,7 @@ (**********************************************************************) Require Import Program. -Require Import Equations Bvector List. +Require Import Equations Vector List. Require Import Relations. Require Import Lia. Require Import Arith Wf_nat. diff --git a/test-suite/issues/issue43.v b/test-suite/issues/issue43.v index 832e6d33a..8c7a6a874 100644 --- a/test-suite/issues/issue43.v +++ b/test-suite/issues/issue43.v @@ -1,4 +1,5 @@ -Require Import Program Bvector List. +Require Import Program List. +Require Vector. Import Vector.VectorNotations. Require Import Relations. From Equations Require Import Equations DepElimDec. diff --git a/test-suite/noconf_hom.v b/test-suite/noconf_hom.v index 7afee5f18..6cc926209 100644 --- a/test-suite/noconf_hom.v +++ b/test-suite/noconf_hom.v @@ -1,5 +1,6 @@ -Require Import Program Bvector List Relations. +Require Import Program List Relations. +Require Vector. Import Vector.VectorNotations. From Equations Require Import Equations Signature DepElimDec. Require Import Utf8. Unset Equations WithK. diff --git a/test-suite/nolam.v b/test-suite/nolam.v index 5a72662b7..6dd659673 100644 --- a/test-suite/nolam.v +++ b/test-suite/nolam.v @@ -6,7 +6,7 @@ (* GNU Lesser General Public License Version 2.1 *) (**********************************************************************) -Require Import Bvector List Relations. +Require Import List Relations. From Equations Require Import Equations Signature. Require Import Utf8. Import ListNotations. diff --git a/test-suite/rec.v b/test-suite/rec.v index bae66b67a..8c559bd84 100644 --- a/test-suite/rec.v +++ b/test-suite/rec.v @@ -7,7 +7,7 @@ (**********************************************************************) Require Import Program Utf8. Require Import Equations.Prop.Equations. -Require Import Bvector List Relations. +Require Import Vector List Relations. Require Import Arith Wf_nat. Require Import Lia. diff --git a/theories/Prop/NoConfusion.v b/theories/Prop/NoConfusion.v index e5f8e8fbc..91b963049 100644 --- a/theories/Prop/NoConfusion.v +++ b/theories/Prop/NoConfusion.v @@ -10,7 +10,7 @@ [equations] when it needs applications of injectivity or discrimination on some equation. *) -Require Import Coq.Program.Tactics Bvector List. +Require Import Coq.Program.Tactics Vector List. From Equations Require Import Init Signature. Require Import Equations.CoreTactics. Require Import Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.Constants.