Simplification and improvement of "subst x" in such a way that it

works in the presence of local definitions referring to x and
dependent in other hyps or concl.

3 files changed, 23 insertions, 24 deletions

diff --git a/CHANGES b/CHANGES
index 3577887537..9269160ddd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -55,7 +55,7 @@ Notations
 - The syntax "x -> y" is now declared at level 99. In particular, it has
   now a lower priority than "<->": "A -> B <-> C" is now "A -> (B <-> C)"
   (possible source of incompatibilities)
-- Notations accept term-provinding tactics using the $(...)$ syntax.
+- Notations accept term-providing tactics using the $(...)$ syntax.
 
 Specification Language
 
@@ -109,6 +109,7 @@ Tactics
 - Injection now also deduces equality of arguments of sort Prop. Old behavior
   can be restored by "Unset Injection On Proofs". Also improved the error
   messages.
+- Tactic "subst id" now supports id occurring in dependent local definitions.
 
 Program
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6e4f46c676..ad54fca233 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1612,35 +1612,24 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
   let hyps = Proofview.Goal.hyps gl in
   let concl = Proofview.Goal.concl gl in
   (* The set of hypotheses using x *)
-  let depdecls =
-    let test (id,_,c as dcl) =
-      if not (Id.equal id hyp) && occur_var_in_decl env x dcl then Some dcl
-      else None in
-    List.rev (List.map_filter test hyps) in
-  let dephyps = List.map (fun (id,_,_) -> id) depdecls in
+  let dephyps =
+    List.rev (snd (List.fold_right (fun (id,b,_ as dcl) (deps,allhyps) ->
+      if not (Id.equal id hyp)
+         && List.exists (fun y -> occur_var_in_decl env y dcl) deps
+      then
+        ((if b = None then deps else id::deps), id::allhyps)
+      else
+        (deps,allhyps))
+      hyps
+      ([x],[]))) in
   (* Decides if x appears in conclusion *)
   let depconcl = occur_var env x concl in
-  (* The set of non-defined hypothesis: they must be abstracted,
-     rewritten and reintroduced *)
-  let abshyps =
-    List.map_filter (function (id, None, _) -> Some (mkVar id) | _ -> None)
-      depdecls in
-  (* a tactic that either introduce an abstracted and rewritten hyp,
-     or introduce a definition where x was replaced *)
-  let introtac = function
-      (id,None,_) -> intro_using id
-    | (id,Some hval,htyp) ->
-        letin_tac None (Name id)
-	  (replace_term (mkVar x) rhs hval)
-	  (Some (replace_term (mkVar x) rhs htyp)) nowhere
-  in
   let need_rewrite = not (List.is_empty dephyps) || depconcl in
   tclTHENLIST
     ((if need_rewrite then
-      [Proofview.V82.tactic (generalize abshyps);
+      [Proofview.V82.tactic (revert dephyps);
        general_rewrite dir AllOccurrences true dep_proof_ok (mkVar hyp);
-       Proofview.V82.tactic (thin dephyps);
-       (tclMAP introtac depdecls)]
+       (tclMAP intro_using dephyps)]
       else
        [Proofview.tclUNIT ()]) @
      [tclTRY (clear [x; hyp])])
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 08c406be94..0e1e778635 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -129,3 +129,12 @@ intros.
 Fail rewrite H in H0.
 Abort.
 
+(* Test subst in the presence of a dependent let-in *)
+(* Was not working prior to May 2014 *)
+
+Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x.
+intros.
+subst x. (* was failing *)
+rewrite H0.
+reflexivity.
+Qed.