Making Evarutil.new_evar monotonous.

3 files changed, 33 insertions, 35 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index c3fe6b6574..3d544274d2 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -14,6 +14,7 @@ open Tacexpr
 open Refiner
 open Evd
 open Locus
+open Sigma.Notations
 
 (* The instantiate tactic *)
 
@@ -76,7 +77,9 @@ let let_evar name typ =
       let id = Namegen.id_of_name_using_hdchar env typ name in
       Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
     | Names.Name id -> id in
-    let sigma',evar = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (evar, sigma', _) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+      let sigma' = Sigma.to_evar_map sigma' in
     Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
       (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
   end
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1b6ba56e66..7e0182137a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -85,7 +85,9 @@ let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
   let s = Typeclasses.set_resolvable Evd.Store.empty false in
-  let evd', t = Evarutil.new_evar ~store:s env evd t in
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (t, evd', _) = Evarutil.new_evar ~store:s env evd t in
+  let evd' = Sigma.to_evar_map evd' in
   let ev, _ = destEvar t in
     (evd', Evar.Set.add ev cstrs), t
 
@@ -1510,12 +1512,11 @@ let assert_replacing id newt tac =
     in
     let env' = Environ.reset_with_named_context (val_of_named_context nc) env in
     Proofview.Refine.refine ~unsafe:false { run = begin fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
-      let sigma, ev = Evarutil.new_evar env' sigma concl in
-      let sigma, ev' = Evarutil.new_evar env sigma newt in
+      let Sigma (ev, sigma, p) = Evarutil.new_evar env' sigma concl in
+      let Sigma (ev', sigma, q) = Evarutil.new_evar env sigma newt in
       let map (n, _, _) = if Id.equal n id then ev' else mkVar n in
       let (e, _) = destEvar ev in
-      Sigma.Unsafe.of_pair (mkEvar (e, Array.map_of_list map nc), sigma)
+      Sigma (mkEvar (e, Array.map_of_list map nc), sigma, p +> q)
     end }
   end in
   Proofview.tclTHEN prf (Proofview.tclFOCUS 2 2 tac)
@@ -1546,9 +1547,8 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
             Proofview.Goal.enter begin fun gl ->
             let env = Proofview.Goal.env gl in
             let make = { run = begin fun sigma ->
-              let sigma = Sigma.to_evar_map sigma in
-              let (sigma, ev) = Evarutil.new_evar env sigma newt in
-              Sigma.Unsafe.of_pair (mkApp (p, [| ev |]), sigma)
+              let Sigma (ev, sigma, q) = Evarutil.new_evar env sigma newt in
+              Sigma (mkApp (p, [| ev |]), sigma, q)
             end } in
             Proofview.Refine.refine ~unsafe:false make <*> Proofview.Unsafe.tclNEWGOALS gls
             end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 90e4f8521e..8a8b36a9e4 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -217,9 +217,10 @@ let convert_concl ?(check=true) ty k =
           if not b then error "Not convertible.";
           sigma
         end else sigma in
-      let (sigma,x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (x, sigma, p) = Evarutil.new_evar env sigma ~principal:true ~store ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
-      Sigma.Unsafe.of_pair (ans, sigma)
+      Sigma (ans, sigma, p)
     end }
   end
 
@@ -232,9 +233,7 @@ let convert_hyp ?(check=true) d =
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
     Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
-      let (sigma, c) = Evarutil.new_evar env sigma ~principal:true ~store ty in
-      Sigma.Unsafe.of_pair (c, sigma)
+      Evarutil.new_evar env sigma ~principal:true ~store ty
     end }
   end
 
@@ -1058,11 +1057,10 @@ let cut c =
       (** Backward compat: normalize [c]. *)
       let c = local_strong whd_betaiota sigma c in
       Proofview.Refine.refine ~unsafe:true { run = begin fun h ->
-        let h = Sigma.to_evar_map h in
-        let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
-        let (h, x) = Evarutil.new_evar env h c in
+        let Sigma (f, h, p) = Evarutil.new_evar ~principal:true env h (mkArrow c (Vars.lift 1 concl)) in
+        let Sigma (x, h, q) = Evarutil.new_evar env h c in
         let f = mkLambda (Name id, c, mkApp (Vars.lift 1 f, [|mkRel 1|])) in
-        Sigma.Unsafe.of_pair (mkApp (f, [|x|]), h)
+        Sigma (mkApp (f, [|x|]), h, p +> q)
       end }
     else
       Tacticals.New.tclZEROMSG (str "Not a proposition or a type.")
@@ -1712,12 +1710,11 @@ let cut_and_apply c =
         let concl = Proofview.Goal.concl gl in
         let env = Tacmach.New.pf_env gl in
         Proofview.Refine.refine { run = begin fun sigma ->
-          let sigma = Sigma.to_evar_map sigma in
           let typ = mkProd (Anonymous, c2, concl) in
-          let (sigma, f) = Evarutil.new_evar env sigma typ in
-          let (sigma, x) = Evarutil.new_evar env sigma c1 in
+          let Sigma (f, sigma, p) = Evarutil.new_evar env sigma typ in
+          let Sigma (x, sigma, q) = Evarutil.new_evar env sigma c1 in
           let ans = mkApp (f, [|mkApp (c, [|x|])|]) in
-          Sigma.Unsafe.of_pair (ans, sigma)
+          Sigma (ans, sigma, p +> q)
         end }
       | _ -> error "lapply needs a non-dependent product."
   end
@@ -1858,9 +1855,7 @@ let clear_body ids =
     in
     check_hyps <*> check_concl <*>
     Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-      let sigma = Sigma.to_evar_map sigma in
-      let (sigma, c) = Evarutil.new_evar env sigma concl in
-      Sigma.Unsafe.of_pair (c, sigma)
+      Evarutil.new_evar env sigma concl
     end }
   end
 
@@ -2432,12 +2427,14 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [heq,None,eq;id,body,t] lastlhyp env in
-      let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
-      Sigma.Unsafe.of_pair (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma)
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in
+      Sigma (mkNamedLetIn id c t (mkNamedLetIn heq refl eq x), sigma, p)
   | None ->
       let newenv = insert_before [id,body,t] lastlhyp env in
-      let (sigma,x) = new_evar newenv sigma ~principal:true ~store ccl in
-      Sigma.Unsafe.of_pair (mkNamedLetIn id c t x, sigma)
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (x, sigma, p) = new_evar newenv sigma ~principal:true ~store ccl in
+      Sigma (mkNamedLetIn id c t x, sigma, p)
 
 let letin_tac with_eq id c ty occs =
   Proofview.Goal.nf_enter begin fun gl ->
@@ -2511,9 +2508,8 @@ let bring_hyps hyps =
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (instance_from_named_context hyps) in
       Proofview.Refine.refine { run = begin fun sigma ->
-        let sigma = Sigma.to_evar_map sigma in
-        let (sigma, ev) = Evarutil.new_evar env sigma newcl in
-        Sigma.Unsafe.of_pair (mkApp (ev, args), sigma)
+        let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in
+        Sigma (mkApp (ev, args), sigma, p)
       end }
     end
 
@@ -2624,9 +2620,8 @@ let new_generalize_gen_let lconstr =
     in
       Proofview.Unsafe.tclEVARS sigma <*>
 	Proofview.Refine.refine { run = begin fun sigma ->
-          let sigma = Sigma.to_evar_map sigma in
-          let (sigma, ev) = Evarutil.new_evar env sigma newcl in
-          Sigma.Unsafe.of_pair ((applist (ev, args)), sigma)
+          let Sigma (ev, sigma, p) = Evarutil.new_evar env sigma newcl in
+          Sigma ((applist (ev, args)), sigma, p)
 	end }
   end