Fixes #8553 (regression of tactic "change" under binders).

5 files changed, 23 insertions, 9 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7298342e1e..633d98a585 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -713,7 +713,7 @@ let mkDestructEq :
     observe_tclTHENLIST (str "mkDestructEq")
      [Proofview.V82.of_tactic (generalize new_hyps);
       (fun g2 ->
-        let changefun patvars sigma =
+        let changefun patvars env sigma =
           pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)
         in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9f34df4608..f90e889678 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -283,6 +283,12 @@ let debugging_exception_step ist signal_anomaly e pp =
   debugging_step ist (fun () ->
     pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
+let ensure_freshness env =
+  (* We anonymize declarations which we know will not be used *)
+  (* This assumes that the original context had no rels *)
+  process_rel_context
+    (fun d e -> EConstr.push_rel (Context.Rel.Declaration.set_name Anonymous d) e) env
+
 (* Raise Not_found if not in interpretation sign *)
 let try_interp_ltac_var coerce ist env {loc;v=id} =
   let v = Id.Map.find id ist.lfun in
@@ -1740,15 +1746,15 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp patvars sigma =
+        let c_interp patvars env sigma =
 	  let lfun' = Id.Map.fold (fun id c lfun ->
 	    Id.Map.add id (Value.of_constr c) lfun) 
 	    patvars ist.lfun
 	  in
 	  let ist = { ist with lfun = lfun' } in
             if is_onhyps && is_onconcl
-            then interp_type ist (pf_env gl) sigma c
-            else interp_constr ist (pf_env gl) sigma c
+            then interp_type ist env sigma c
+            else interp_constr ist env sigma c
         in
         Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl)
       end
@@ -1761,11 +1767,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
         let sigma = project gl in
         let op = interp_typed_pattern ist env sigma op in
         let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in
-        let c_interp patvars sigma =
+        let c_interp patvars env sigma =
           let lfun' = Id.Map.fold (fun id c lfun ->
             Id.Map.add id (Value.of_constr c) lfun) 
             patvars ist.lfun
           in
+          let env = ensure_freshness env in
           let ist = { ist with lfun = lfun' } in
             try
               interp_constr ist env sigma c
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6999b17d8e..f3f81ff616 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -791,9 +791,9 @@ let e_change_in_hyp redfun (id,where) =
     (convert_hyp c)
   end
 
-type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr
+type change_arg = Ltac_pretype.patvar_map -> env -> evar_map -> evar_map * EConstr.constr
 
-let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
+let make_change_arg c pats env sigma = (sigma, replace_vars (Id.Map.bindings pats) c)
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -818,7 +818,7 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
 
 (* Now we introduce different instances of the previous tacticals *)
 let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
-  let (sigma, t') = t sigma in
+  let (sigma, t') = t env sigma in
   let sigma = check_types env sigma mayneedglobalcheck deep t' c in
   match infer_conv ~pb:cv_pb env sigma t' c with
   | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c088e404b0..24c12ffd82 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -145,7 +145,7 @@ val exact_proof      : Constrexpr.constr_expr -> unit Proofview.tactic
 type tactic_reduction = Reductionops.reduction_function
 type e_tactic_reduction = Reductionops.e_reduction_function
 
-type change_arg = patvar_map -> evar_map -> evar_map * constr
+type change_arg = patvar_map -> env -> evar_map -> evar_map * constr
 
 val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> unit Proofview.tactic
diff --git a/test-suite/bugs/closed/8553.v b/test-suite/bugs/closed/8553.v
new file mode 100644
index 0000000000..4a1afabe89
--- /dev/null
+++ b/test-suite/bugs/closed/8553.v
@@ -0,0 +1,7 @@
+(* Using tactic "change" under binders *)
+
+Definition add2 n := n +2.
+Goal (fun n => n) = (fun n => n+2).
+change (?n + 2) with (add2 n).
+match goal with |- _ = (fun n => add2 n) => idtac end. (* To test the presence of add2 *)
+Abort.