diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 12:51:59 +0000 |
| commit | 4c3301517cf8887b3684fda58e2e4626a072a5fb (patch) | |
| tree | bd1ed746e255a9f25b486711163001b2f45d8017 /theories/Program/Wf.v | |
| parent | a8b034513e0c03ceb7e154949b15f62ac6862f3b (diff) | |
Various fixes:
- Fix a typo in lowercase_utf8
- Fix generation of signatures in subtac_cases not working for dependent
inductive types with dependent indices.
- Fix coercion of inductive types generating ill-typed terms.
- Fix test script using new syntax for Instances.
- Move simpl_existTs to Program.Equality and use it in simpl_depind.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10932 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Wf.v')
| -rw-r--r-- | theories/Program/Wf.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index cbc3b02ad..b6ba5d44e 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -50,9 +50,6 @@ Section Well_founded. Lemma Fix_F_inv : forall (x:A) (r s:Acc R x), Fix_F x r = Fix_F x s. Proof. intro x; induction (Rwf x); intros. - rewrite <- (Fix_F_eq x r); rewrite <- (Fix_F_eq x s); intros. - apply F_ext; auto. - intros. rewrite (proof_irrelevance (Acc R x) r s) ; auto. Qed. |