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/Program/Equality.v | 5 ----- theories/Program/Syntax.v | 11 ----------- 2 files changed, 16 deletions(-) (limited to 'theories/Program') 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. -- cgit v1.2.3