diff options
| author |  marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-09 16:39:01 +0000 |
|---|---|---|
| committer | marche <marche@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-02-09 16:39:01 +0000 |
| commit | 5f547a9465e629d30ecce3da74090334dbdb63bf (patch) | |
| tree | 1054380ffac7547b70a2221cef273911cbcaf2a7 /theories/Bool/Bvector.v | |
| parent | 7218dde04726bdcbf86dde85e14996669e0c7e94 (diff) | |
patch Bvector: args implicites
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5309 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Bool/Bvector.v')
| -rw-r--r-- | theories/Bool/Bvector.v | 7 |
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. |