aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Vectors
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Vectors')
-rw-r--r--theories/Vectors/VectorDef.v8
1 files changed, 0 insertions, 8 deletions
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 807748edd..cff72c11b 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -269,14 +269,6 @@ end.
End ITERATORS.
-Implicit Arguments rectS.
-Implicit Arguments rect2.
-Implicit Arguments fold_left.
-Implicit Arguments fold_right.
-Implicit Arguments map.
-Implicit Arguments fold_left2.
-
-
Section SCANNING.
Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
|Forall_nil: Forall P []