diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-23 14:08:35 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-23 14:08:35 +0000 |
| commit | 54203b86a973f05326153b40c850c6a9c00b23b6 (patch) | |
| tree | 2258a89eb5ac95f862dd0664f24d06ed153fe65a /theories/Logic/JMeq.v | |
| parent | c4d79461518f5dd4351a558cac4c3d3ad410609a (diff) | |
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
Diffstat (limited to 'theories/Logic/JMeq.v')
| -rw-r--r-- | theories/Logic/JMeq.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index 4e9f46b7c..583d348a2 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -24,6 +24,8 @@ Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop := Set Elimination Schemes. +Implicit Arguments JMeq_refl [[A] [x]] [A]. + Hint Resolve JMeq_refl. Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x. |