Fix #3590 for good this time, by changing the API, change's argument now

takes a variable substitution for matched variables in the (lhs) pattern, and
uses the existing ist structure to pretype the rhs correcly, without
having to deal with the volatile evars.

4 files changed, 24 insertions, 16 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index bcfd6657e..7ab8d0c3b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1493,10 +1493,10 @@ let cutSubstInHyp l2r eqn id =
   tclTHENFIRST
     (tclTHENLIST [
        (Proofview.Unsafe.tclEVARS sigma);
-       (change_in_hyp None (fun s -> s,typ) (id,InHypTypeOnly));
+       (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly));
        (replace_core (onHyp id) l2r eqn)
     ])
-    (change_in_hyp None (fun s -> s,expected) (id,InHypTypeOnly))
+    (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly))
   end
 
 let try_rewrite tac =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f894eb8fc..5406832d2 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2119,7 +2119,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp sigma =
+        let c_interp patvars 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
@@ -2139,7 +2144,12 @@ and interp_atomic ist tac : unit Proofview.tactic =
           let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
           let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
 	  let env' = Environ.push_named_context sign env in
-          let c_interp sigma =
+          let c_interp patvars 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
 	      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 b1559da33..7484139c6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -584,7 +584,10 @@ let e_change_in_hyp redfun (id,where) =
       (Proofview.Goal.env gl) (Proofview.Goal.sigma gl))
     convert_hyp
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr
+
+let make_change_arg c =
+  fun pats 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
@@ -612,21 +615,15 @@ let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
   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' 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
-
 (* Use cumulativity only if changing the conclusion not a subterm *)
 let change_on_subterm cv_pb deep t where env sigma c =
   let mayneedglobalcheck = ref false in
   let sigma,c = match where with
-  | None -> change_and_check cv_pb mayneedglobalcheck deep t env sigma c
+  | None -> change_and_check cv_pb mayneedglobalcheck deep (t Id.Map.empty) env sigma c
   | Some occl ->
       e_contextually false occl
         (fun subst ->
-          change_and_check_subst Reduction.CONV mayneedglobalcheck subst t)
+          change_and_check Reduction.CONV mayneedglobalcheck true (t subst))
         env sigma c in
   if !mayneedglobalcheck then
     begin
@@ -656,7 +653,7 @@ let change chg c cls gl =
     cls) gl
 
 let change_concl t = 
-  change_in_concl None (fun sigma -> sigma, t)
+  change_in_concl None (make_change_arg t)
 
 (* Pour usage interne (le niveau User est pris en compte par reduce) *)
 let red_in_concl        = reduct_in_concl (red_product,REVERTcast)
@@ -2769,7 +2766,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac =
     if Int.equal i nparams then
       let t = applist (hd, params@args) in
       Tacticals.New.tclTHEN
-        (change_in_hyp None (fun sigma -> sigma, t) (hyp0,InHypTypeOnly))
+        (change_in_hyp None (make_change_arg t) (hyp0,InHypTypeOnly))
         (tac avoid)
     else
       let c = List.nth argl (i-1) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index eea495621..0069d100b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -125,8 +125,9 @@ val exact_proof      : Constrexpr.constr_expr -> tactic
 
 type tactic_reduction = env -> evar_map -> constr -> constr
 
-type change_arg = evar_map -> evar_map * constr
+type change_arg = patvar_map -> evar_map -> evar_map * constr
 
+val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic
 val reduct_option     : ?check:bool -> tactic_reduction * cast_kind -> goal_location -> tactic
 val reduct_in_concl   : tactic_reduction * cast_kind -> tactic