aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool')
-rw-r--r--theories/Bool/Bvector.v7
1 files changed, 5 insertions, 2 deletions
diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v
index 86b59db26..aa69fccf1 100644
--- a/theories/Bool/Bvector.v
+++ b/theories/Bool/Bvector.v
@@ -196,6 +196,9 @@ Defined.
End VECTORS.
+Implicit Arguments Vnil [A].
+Implicit Arguments Vcons [A n].
+
Section BOOLEAN_VECTORS.
(*
@@ -212,9 +215,9 @@ ATTENTION : Tous les décalages prennent la taille moins un comme paramètre
Definition Bvector := vector bool.
-Definition Bnil := Vnil bool.
+Definition Bnil := @Vnil bool.
-Definition Bcons := Vcons bool.
+Definition Bcons := @Vcons bool.
Definition Bvect_true := Vconst bool true.