diff options
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Equality.v | 5 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 11 |
2 files changed, 0 insertions, 16 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 2f0185eac..d678757d9 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -37,11 +37,6 @@ Ltac unblock_goal := unfold block in *. Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). -(** Notation for the single element of [x = x] and [x ~= x]. *) - -Implicit Arguments eq_refl [[A] [x]] [A]. -Implicit Arguments JMeq_refl [[A] [x]] [A]. - (** Do something on an heterogeneous equality appearing in the context. *) Ltac on_JMeq tac := 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. |