From 54203b86a973f05326153b40c850c6a9c00b23b6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 23 Oct 2010 14:08:35 +0000 Subject: Used multiple lists of implicit arguments to transfer the choices of Program in terms of implicit arguments to the rest of the library. This commit only covers the case of list of implicit arguments that have a different length in Program (e.g. inl, Vcons) but not the case of implicit arguments which differs only in their maximality status (e.g. pair). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13575 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Bool/Bvector.v | 3 +++ 1 file changed, 3 insertions(+) (limited to 'theories/Bool') diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index 88bc15c69..694ed15b4 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -249,3 +249,6 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := end. End BOOLEAN_VECTORS. + +Implicit Arguments Vcons [[A] [n]] []. +Implicit Arguments Vnil [[A]] []. -- cgit v1.2.3