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.

1 files changed, 12 insertions, 2 deletions

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.")