Require Vector directly instead of through Bvector

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`.
 
-*)
+*)

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]. *)
 

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 ;

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 := .

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

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.

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.
 

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.

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.

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.
 

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.