diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-29 17:24:44 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-29 17:24:44 +0000 |
| commit | 5489f356bdd7d1bc8511e3d2e4e5753373057b5f (patch) | |
| tree | d7a3ce58e9896add5507104ae34e2b07166c5799 /theories | |
| parent | f9f59c8e1ea2e8d43d491a0ebf4c3fbea87026d2 (diff) | |
modification de la definition des def inductives unitaires et autorisation d'elimination sur la sorte Type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
| -rwxr-xr-x | theories/Init/Logic.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 35b326d17..14c8a95a2 100755 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -165,6 +165,7 @@ Section Logic_lemmas. End equality. +(* Is now a primitive principle Theorem eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(eq ? x y)->(P y). Proof. Intros. @@ -172,6 +173,7 @@ Section Logic_lemmas. NewDestruct 1; Auto. Elim H; Auto. Qed. +*) Definition eq_ind_r : (A:Set)(x:A)(P:A->Prop)(P x)->(y:A)(eq ? y x)->(P y). Intros A x P H y H0; Case sym_eq with 1:= H0; Trivial. |