Monotonizing Tactics.change_arg.

4 files changed, 29 insertions, 16 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 685a5e8bd..dd5381c76 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -38,6 +38,7 @@ open Auto
 open Eauto
 
 open Indfun_common
+open Sigma.Notations
 
 
 
@@ -687,9 +688,12 @@ let mkDestructEq :
     observe_tclTHENLIST (str "mkDestructEq")
      [Simple.generalize new_hyps;
       (fun g2 ->
-	Proofview.V82.of_tactic (change_in_concl None
-	  (fun patvars sigma ->
-	    pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2))) g2);
+        let changefun patvars = { run = fun sigma ->
+          let sigma = Sigma.to_evar_map sigma in
+          let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in
+          Sigma.Unsafe.of_pair (c, sigma)
+        } in
+	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
 
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1673aac0a..b3a17df36 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2147,16 +2147,20 @@ and interp_atomic ist tac : unit Proofview.tactic =
           | AllOccurrences | NoOccurrences -> true
           | _ -> false
         in
-        let c_interp patvars sigma =
+        let c_interp patvars = { Sigma.run = begin fun sigma ->
 	  let lfun' = Id.Map.fold (fun id c lfun ->
 	    Id.Map.add id (Value.of_constr c) lfun) 
 	    patvars ist.lfun
 	  in
+	  let sigma = Sigma.to_evar_map sigma 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
-        in
+	  let (sigma, c) =
+            if is_onhyps && is_onconcl
+            then interp_type ist (pf_env gl) sigma c
+            else interp_constr ist (pf_env gl) sigma c
+          in
+          Sigma.Unsafe.of_pair (c, sigma)
+        end } in
 	  (Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl))
           gl
       end
@@ -2171,16 +2175,19 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Proofview.V82.tactic begin fun gl -> 
           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 c_interp patvars sigma =
+          let c_interp patvars = { Sigma.run = begin fun 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
+	      try
+                let sigma = Sigma.to_evar_map sigma in
+                let (sigma, c) = interp_constr ist env sigma c in
+                Sigma.Unsafe.of_pair (c, sigma)
 	      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.")
-          in
+          end } in
 	    (Tactics.change (Some op) c_interp (interp_clause ist env sigma cl))
 	      { gl with sigma = sigma }
         end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 62f306927..fc453cfaf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -642,10 +642,10 @@ let e_change_in_hyp redfun (id,where) =
     Sigma.Unsafe.of_pair (convert_hyp c, sigma)
   end }
 
-type change_arg = Pattern.patvar_map -> evar_map -> evar_map * constr
+type change_arg = Pattern.patvar_map -> constr Sigma.run
 
-let make_change_arg c =
-  fun pats sigma -> (sigma, replace_vars (Id.Map.bindings pats) c)
+let make_change_arg c pats =
+  { run = fun sigma -> Sigma.here (replace_vars (Id.Map.bindings pats) c) sigma }
 
 let check_types env sigma mayneedglobalcheck deep newc origc =
   let t1 = Retyping.get_type_of env sigma newc in
@@ -667,7 +667,9 @@ 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 = Sigma.Unsafe.of_evar_map sigma in
+  let Sigma (t', sigma, p) = t.run sigma in
+  let sigma = Sigma.to_evar_map 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.");
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index d62d27ca3..8a4717b7b 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 = patvar_map -> evar_map -> evar_map * constr
+type change_arg = patvar_map -> constr Sigma.run
 
 val make_change_arg   : constr -> change_arg
 val reduct_in_hyp     : ?check:bool -> tactic_reduction -> hyp_location -> tactic