The Coq mailing list

[S�bastien Hinderer <Sebastien.Hinderer AT ens-lyon.fr>]

Dear Coq users and developers,

Please find attached to this mail a patch you can apply to the Bvector
module which is part of Coq's standard library.
It declares [A] as an implicit argument for Vnil and [A n] as implicit
arguments for Vcons.
Not very hard to write, but so useful when working with vectors.

It's a patch agains coq-8.0beta. To apply, do :

cd $COQTOP/theories/Boolean
patch -p0 < Bvector-patch

Hope this helps.
Sébastien.
--- Bvector.v   2004-02-06 17:32:18.000000000 +0100
+++ Bvector2.v  2004-02-06 15:59:23.000000000 +0100
@@ -196,6 +196,9 @@
 
 End VECTORS.
 
+Implicit Arguments Vnil [A].
+Implicit Arguments Vcons [A n].
+
 Section BOOLEAN_VECTORS.
 
 (* 
@@ -212,9 +215,9 @@
 
 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.