diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-03 13:12:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-03 13:12:11 +0000 |
| commit | 4a452a508a6c411599d6f34bafdec41a3e1d8303 (patch) | |
| tree | 61dc105ea02aeb7853fba203299295045ad9bda2 /theories/Init/Wf.v | |
| parent | b82cb93d2020783f72a8f99142799b51ca7991a9 (diff) | |
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
Diffstat (limited to 'theories/Init/Wf.v')
| -rw-r--r-- | theories/Init/Wf.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v index 3c16b058a..2bb7eae94 100644 --- a/theories/Init/Wf.v +++ b/theories/Init/Wf.v @@ -34,6 +34,8 @@ Section Well_founded. destruct 1; trivial. Defined. + Global Implicit Arguments Acc_inv [x y] [x]. + (** A relation is well-founded if every element is accessible *) Definition well_founded := forall a:A, Acc a. |