diff options
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. |