Revision 12557 continued (better rendering of dependent rewrite)

(expected goal was not correct for rewriting in hypotheses)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12580 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 23 insertions, 11 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index c5ffe72b4d..b0570215ac 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1096,16 +1096,14 @@ let swapEquandsInConcl gls =
 
 (* Refine from [|- P e2] to [|- P e1] and [|- e1=e2:>t] (body is P (Rel 1)) *)
 
-let bareRevSubstInConcl lbeq body expected_goal (t,e1,e2) gls =
+let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
   (* find substitution scheme *)
   let eq_elim = find_elim lbeq.eq (Some false) false None [e1;e2] gls in
   (* build substitution predicate *)
   let p = lambda_create (pf_env gls) (t,body) in
   (* apply substitution scheme *)
-  refine (applist(eq_elim,
-    [t;e1;p;
-     mkCast(Evarutil.mk_new_meta(),DEFAULTcast,expected_goal);
-     e2;Evarutil.mk_new_meta()])) gls
+  refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta();
+                           e2;Evarutil.mk_new_meta()])) gls
 
 (* [subst_tuple_term dep_pair B]
 
@@ -1173,7 +1171,9 @@ let cutSubstInConcl_RL eqn gls =
   let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
   let body,expected_goal = pf_apply subst_tuple_term gls e2 e1 (pf_concl gls) in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  bareRevSubstInConcl lbeq body expected_goal eq gls
+  tclTHENFIRST
+    (bareRevSubstInConcl lbeq body eq)
+    (convert_concl expected_goal DEFAULTcast) gls
 
 (* |- (P e1)
      BY CutSubstInConcl_LR (eq T e1 e2)
@@ -1192,8 +1192,8 @@ let cutSubstInHyp_LR eqn id gls =
   let idtyp = pf_get_hyp_typ gls id in
   let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in
   if not (dependent (mkRel 1) body) then raise NothingToRewrite;
-  cut_replacing id (subst1 e2 body)
-    (tclTHENFIRST (bareRevSubstInConcl lbeq body expected_goal eq)) gls
+  cut_replacing id expected_goal
+    (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls
 
 let cutSubstInHyp_RL eqn id gls =
   (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id)
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index b06718251e..9bc6800724 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -39,7 +39,7 @@ intros n H.
 rewrite plus_0_l in H.
 Abort.
 
-(* Dependent rewrite from left-to-right *)
+(* Rewrite dependent proofs from left-to-right *)
 
 Lemma l1 :
   forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
@@ -49,7 +49,7 @@ rewrite H in H0.
 assumption.
 Qed.
 
-(* Dependent rewrite from right-to-left *)
+(* Rewrite dependent proofs from right-to-left *)
 
 Lemma l2 :
   forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
@@ -59,7 +59,7 @@ rewrite <- H in H0.
 assumption.
 Qed.
 
-(* Check dependent rewriting with non-symmetric equalities *)
+(* Check rewriting dependent proofs with non-symmetric equalities *)
 
 Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H.
 intros x H P H0.
@@ -68,3 +68,15 @@ rewrite H in H0.
 assumption.
 Qed.
 
+(* Dependent rewrite *)
+
+Require Import JMeq.
+
+Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.  
+inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3.
+Undo.
+intros; inversion H; dependent rewrite H4 in H0.
+Undo.
+intros; inversion H; dependent rewrite <- H4 in H0.
+Abort.
+