diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-23 14:08:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-23 14:08:35 +0000 |
| commit | 54203b86a973f05326153b40c850c6a9c00b23b6 (patch) | |
| tree | 2258a89eb5ac95f862dd0664f24d06ed153fe65a /theories/Program/Syntax.v | |
| parent | c4d79461518f5dd4351a558cac4c3d3ad410609a (diff) | |
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
Diffstat (limited to 'theories/Program/Syntax.v')
| -rw-r--r-- | theories/Program/Syntax.v | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index fb8dc087b..d66785874 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -21,12 +21,6 @@ Notation " () " := tt. Implicit Arguments Some [[A]]. Implicit Arguments None [[A]]. -Implicit Arguments inl [[A] [B]] [A]. -Implicit Arguments inr [[A] [B]] [B]. - -Implicit Arguments left [[A] [B]] [A]. -Implicit Arguments right [[A] [B]] [B]. - Implicit Arguments pair [[A] [B]]. Implicit Arguments fst [[A] [B]]. Implicit Arguments snd [[A] [B]]. @@ -40,13 +34,8 @@ Notation " [ ] " := nil : list_scope. Notation " [ x ] " := (cons x nil) : list_scope. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -(** Implicit arguments for vectors. *) - Require Import Bvector. -Implicit Arguments Vnil [[A]] []. -Implicit Arguments Vcons [[A] [n]] []. - (** Treating n-ary exists *) Tactic Notation "exists" constr(x) := exists x. |