From 4a452a508a6c411599d6f34bafdec41a3e1d8303 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 3 Oct 2010 13:12:11 +0000 Subject: Using multiple lists of implicit arguments in Program for preserving the compatibility with the rest of the theories. Used multiple lists of implicit arguments in Init only when the maximality status is not modified in Program (and thus the compatibility is strictly preserved). This improves the compatibility for the implicit arguments of eq_refl and JMeq_refl between 8.2 and 8.3 when using Program (up to the residual differences in the maximality status). For the constants Acc_inv, inl, inr, left, right, Vnil, Vcons, the compatibility with 8.2 is not improved but the consistency between Program and the rest of the library is. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13485 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Program/Equality.v | 4 ++-- theories/Program/Syntax.v | 14 ++++++-------- theories/Program/Wf.v | 2 -- 3 files changed, 8 insertions(+), 12 deletions(-) (limited to 'theories/Program') diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 37c17aa9a..2f0185eac 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -39,8 +39,8 @@ 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]]. -Implicit Arguments JMeq_refl [[A] [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. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index c185ced8f..fb8dc087b 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -18,16 +18,14 @@ Notation " () " := tt. (** Set maximally inserted implicit arguments for standard definitions. *) -Implicit Arguments eq [[A]]. - Implicit Arguments Some [[A]]. Implicit Arguments None [[A]]. -Implicit Arguments inl [[A] [B]]. -Implicit Arguments inr [[A] [B]]. +Implicit Arguments inl [[A] [B]] [A]. +Implicit Arguments inr [[A] [B]] [B]. -Implicit Arguments left [[A] [B]]. -Implicit Arguments right [[A] [B]]. +Implicit Arguments left [[A] [B]] [A]. +Implicit Arguments right [[A] [B]] [B]. Implicit Arguments pair [[A] [B]]. Implicit Arguments fst [[A] [B]]. @@ -46,8 +44,8 @@ Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. Require Import Bvector. -Implicit Arguments Vnil [[A]]. -Implicit Arguments Vcons [[A] [n]]. +Implicit Arguments Vnil [[A]] []. +Implicit Arguments Vcons [[A] [n]] []. (** Treating n-ary exists *) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index abab954af..a823aedd3 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -14,8 +14,6 @@ Require Import ProofIrrelevance. Open Local Scope program_scope. -Implicit Arguments Acc_inv [A R x y]. - Section Well_founded. Variable A : Type. Variable R : A -> A -> Prop. -- cgit v1.2.3