Fixing side bug in db37c9f3f32ae7 delaying interpretation of the

right-hand side of a "change with": the rhs lives in the toplevel
environment.

7 files changed, 25 insertions, 16 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 72613624ba..fd54584bc8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -674,7 +674,7 @@ let mkDestructEq :
      [Simple.generalize new_hyps;
       (fun g2 ->
 	change_in_concl None
-	  (fun env sigma -> 
+	  (fun sigma ->
 	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index cbe1e95316..c537d895d6 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -562,7 +562,7 @@ let autounfold_one db cl gl =
   in
     if did then
       match cl with
-      | Some hyp -> change_in_hyp None (fun env sigma -> sigma, c') hyp gl
+      | Some hyp -> change_in_hyp None (fun sigma -> sigma, c') hyp gl
       | None -> Proofview.V82.of_tactic (convert_concl_no_check c' DEFAULTcast) gl
     else tclFAIL 0 (str "Nothing to unfold") gl
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4da80811bd..d6083860a9 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1500,10 +1500,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (Proofview.V82.tactic (change_in_hyp None (fun _ s -> s,typ) (id,InHypTypeOnly)));
+       (Proofview.V82.tactic (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly)));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (Proofview.V82.tactic (change_in_hyp None (fun _ s -> s,expected) (id,InHypTypeOnly)))
+    (Proofview.V82.tactic (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly)))
   end
 
 let try_rewrite tac =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index bb525ec586..54fbbbe274 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2082,10 +2082,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp env sigma =
+        let c_interp sigma =
 	  if is_onhyps && is_onconcl
-	  then interp_type ist env sigma c
-	  else interp_constr ist env sigma c
+	  then interp_type ist (pf_env gl) sigma c
+	  else interp_constr ist (pf_env gl) sigma c
         in
 	  (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl))
           gl
@@ -2101,8 +2101,8 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Proofview.V82.tactic begin fun gl -> 
           let sign,op = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
-          let c_interp env sigma =
-	    let env' = Environ.push_named_context sign env in
+	  let env' = Environ.push_named_context sign env in
+          let c_interp sigma =
 	      try interp_constr ist env' sigma c
 	      with e when to_catch e (* Hack *) ->
 		errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 34fd8a8beb..c600a86cb4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -586,7 +586,7 @@ let e_change_in_hyp redfun (id,where) gl =
     (e_pf_change_decl redfun where (pf_get_hyp gl id))
     (fun s -> Proofview.V82.of_tactic (convert_hyp s)) gl
 
-type change_arg = env -> evar_map -> evar_map * constr
+type change_arg = evar_map -> evar_map * constr
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -608,15 +608,15 @@ 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 env sigma in
+  let sigma, t' = t sigma in
   check_types env sigma mayneedglobalcheck deep t' c;
   let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
   if not b then errorlabstrm "convert-check-hyp" (str "Not convertible.");
   sigma, t'
 
 let change_and_check_subst cv_pb mayneedglobalcheck subst t env sigma c =
-  let t' env sigma = 
-    let sigma, t = t env sigma in
+  let t' sigma =
+    let sigma, t = t sigma in
       sigma, replace_vars (Id.Map.bindings subst) t 
   in change_and_check cv_pb mayneedglobalcheck true t' env sigma c
 
@@ -658,7 +658,7 @@ let change chg c cls gl =
     cls gl
 
 let change_concl t = 
-  change_in_concl None (fun env sigma -> sigma, t)
+  change_in_concl None (fun sigma -> sigma, t)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
@@ -2747,7 +2747,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
       Proofview.V82.tactic
-        (change_in_hyp None (fun _ sigma -> sigma, t) (hyp0,InHypTypeOnly))
+        (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly))
     else
       let c = List.nth argl (i-1) in
       match kind_of_term c with
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 556a5a3512..75b1fe7044 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -125,7 +125,7 @@ val exact_proof      : Constrexpr.constr_expr -> tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-type change_arg = env -> evar_map -> evar_map * constr
+type change_arg = evar_map -> evar_map * constr
 
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index cd2dd77f9e..1f0b7d38a9 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -50,3 +50,12 @@ Abort.
 Goal nat = nat :> Set.
 Fail change nat with (@id Type nat). (* would otherwise be ill-typed *)
 Abort.
+
+(* Check typing env for rhs is the correct one *)
+
+Goal forall n, let x := n in id (fun n => n + x) 0 = 0.
+intros.
+unfold x.
+(* check that n in 0+n is not interpreted as the n from "fun n" *)
+change n with (0+n).
+Abort.