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

3 files changed, 14 insertions, 15 deletions

diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 0f88fbdd9..b56ca26c3 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -45,6 +45,17 @@ Ltac simpl_one_dep_JMeq :=
 
 Require Import Eqdep.
 
+(** Simplify dependent equality using sigmas to equality of the second projections if possible. 
+   Uses UIP. *)
+
+Ltac simpl_existT :=
+  match goal with
+    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
+    let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
+  end.
+
+Ltac simpl_existTs := repeat simpl_existT.
+
 (** Tries to eliminate a call to [eq_rect] (the substitution principle) by any means available. *)
 
 Ltac elim_eq_rect :=
@@ -213,7 +224,8 @@ Ltac do_simpl_IHs_eqs :=
 
 Ltac simpl_IHs_eqs := repeat do_simpl_IHs_eqs.
 
-Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; simpl_JMeq ; simpl_IHs_eqs.
+Ltac simpl_depind := subst* ; autoinjections ; try discriminates ; 
+  simpl_JMeq ; simpl_existTs ; simpl_IHs_eqs.
 
 (** The following tactics allow to do induction on an already instantiated inductive predicate
    by first generalizing it and adding the proper equalities to the context, in a maner similar to 
@@ -231,7 +243,7 @@ Ltac prepare_depind H :=
    and starts a dependent induction using this tactic. *)
 
 Ltac do_depind tac H :=
-  prepare_depind H ; tac H ; simpl_depind.
+  prepare_depind H ; tac H ; repeat progress simpl_depind.
 
 (** Calls [destruct] on the generalized hypothesis, results should be similar to inversion. *)
 
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c9de1a9e1..d021326a1 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -13,16 +13,6 @@ Open Local Scope program_scope.
 
 (** Tactics related to subsets and proof irrelevance. *)
 
-(** Simplify dependent equality using sigmas to equality of the codomains if possible. *)
-
-Ltac simpl_existT :=
-  match goal with
-    [ H : existT _ ?x _ = existT _ ?x _ |- _ ] => 
-    let Hi := fresh H in assert(Hi:=inj_pairT2 _ _ _ _ _ H) ; clear H
-  end.
-
-Ltac simpl_existTs := repeat simpl_existT.
-
 (** The following tactics implement a poor-man's solution for proof-irrelevance: it tries to 
    factorize every proof of the same proposition in a goal so that equality of such proofs becomes trivial. *)
 
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.