Making Evarutil.new_evar monotonous.

9 files changed, 75 insertions, 57 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d5bb564f6..60d92f4be 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -22,6 +22,7 @@ open Evarsolve
 open Globnames
 open Evd
 open Pretype_errors
+open Sigma.Notations
 
 type unify_fun = transparent_state ->
   env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
@@ -830,7 +831,9 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	      (i,t2::ks, m-1, test)
 	  else
 	    let dloc = (Loc.ghost,Evar_kinds.InternalHole) in
-            let (i',ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
+	    let i = Sigma.Unsafe.of_evar_map i in
+            let Sigma (ev, i', _) = Evarutil.new_evar env i ~src:dloc (substl ks b) in
+            let i' = Sigma.to_evar_map i' in
 	    (i', ev :: ks, m - 1,test))
 	(evd,[],List.length bs,fun i -> Success i) bs
     in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1c3ae9ad9..bc9f08331 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -385,7 +385,7 @@ let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?prin
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
   let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
   let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
   let instance =
@@ -394,9 +394,14 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
     | Some filter -> Filter.filter_list filter instance in
   new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
 
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let evd = Sigma.to_evar_map evd in
+  let (sigma, c) = new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  Sigma.Unsafe.of_pair (c, sigma)
+
 let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
   let evd', s = new_sort_variable rigid evd in
-  let evd', e = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+  let evd', e = new_evar_unsafe env evd' ?src ?filter ?naming ?principal (mkSort s) in
     evd', (e, s)
 
 let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
@@ -414,7 +419,7 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
 
   (* The same using side-effect *)
 let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
-  let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+  let (evd',ev) = new_evar_unsafe env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
   evdref := evd';
   ev
 
@@ -717,7 +722,7 @@ let define_pure_evar_as_product evd evk =
     let filter = Filter.extend 1 (evar_filter evi) in
       if is_prop_sort s then
        (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar newenv evd1 concl ~src ~filter
+        new_evar_unsafe newenv evd1 concl ~src ~filter
       else
 	let evd3, (rng, srng) =
 	  new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
@@ -763,7 +768,7 @@ let define_pure_evar_as_lambda env evd evk =
   let newenv = push_named (id, None, dom) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
   let src = evar_source evk evd1 in
-  let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk lam evd2, lam
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 76d67c748..96648bb11 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -22,10 +22,10 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 val new_evar :
-  env -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
+  env -> 'r Sigma.t -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
   ?candidates:constr list -> ?store:Store.t ->
   ?naming:Misctypes.intro_pattern_naming_expr ->
-  ?principal:bool -> types -> evar_map * constr
+  ?principal:bool -> types -> (constr, 'r) Sigma.sigma
 
 val new_pure_evar :
   named_context_val -> evar_map -> ?src:Loc.t * Evar_kinds.t -> ?filter:Filter.t ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 123f9b8cd..9caa86895 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -27,6 +27,7 @@ open Recordops
 open Locus
 open Locusops
 open Find_subterm
+open Sigma.Notations
 
 let keyed_unification = ref (false)
 let _ = Goptions.declare_bool_option {
@@ -105,7 +106,9 @@ let set_occurrences_of_last_arg args =
   Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args)
 
 let abstract_list_all_with_dependencies env evd typ c l =
-  let evd,ev = new_evar env evd typ in
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (ev, evd, _) = new_evar env evd typ in
+  let evd = Sigma.to_evar_map evd in
   let evd,ev' = evar_absorb_arguments env evd (destEvar ev) l in
   let n = List.length l in
   let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
@@ -1155,20 +1158,20 @@ let merge_instances env sigma flags st1 st2 c1 c2 =
  * close it off.  But this might not always work,
  * since other metavars might also need to be resolved. *)
 
-let applyHead env evd n c  =
-  let rec apprec n c cty evd =
+let applyHead env (type r) (evd : r Sigma.t) n c =
+  let rec apprec : type s. _ -> _ -> _ -> (r, s) Sigma.le -> s Sigma.t -> (constr, r) Sigma.sigma =
+    fun n c cty p evd ->
     if Int.equal n 0 then
-      (evd, c)
+      Sigma (c, evd, p)
     else
-      match kind_of_term (whd_betadeltaiota env evd cty) with
+      match kind_of_term (whd_betadeltaiota env (Sigma.to_evar_map evd) cty) with
       | Prod (_,c1,c2) ->
-        let (evd',evar) =
-	  Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
-	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
+        let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.ghost,Evar_kinds.GoalEvar) c1 in
+	  apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
       | _ -> error "Apply_Head_Then"
   in
-    apprec n c (Typing.unsafe_type_of env evd c) evd
-    
+    apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
+
 let is_mimick_head ts f =
   match kind_of_term f with
   | Const (c,u) -> not (Closure.is_transparent_constant ts c)
@@ -1328,7 +1331,9 @@ let w_merge env with_types flags (evd,metas,evars) =
   and mimick_undefined_evar evd flags hdc nargs sp =
     let ev = Evd.find_undefined evd sp in
     let sp_env = Global.env_of_context ev.evar_hyps in
-    let (evd', c) = applyHead sp_env evd nargs hdc in
+    let evd = Sigma.Unsafe.of_evar_map evd in
+    let Sigma (c, evd', _) = applyHead sp_env evd nargs hdc in
+    let evd' = Sigma.to_evar_map evd' in
     let (evd'',mc,ec) =
       unify_0 sp_env evd' CUMUL flags
         (get_type_of sp_env evd' c) ev.evar_concl in
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 0697c94d7..ae790d9b8 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -24,6 +24,7 @@ open Pretype_errors
 open Evarutil
 open Unification
 open Misctypes
+open Sigma.Notations
 
 (* Abbreviations *)
 
@@ -335,7 +336,9 @@ let clenv_pose_metas_as_evars clenv dep_mvs =
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
-	let (evd,evar) = new_evar (cl_env clenv) clenv.evd ~src ty in
+        let evd = Sigma.Unsafe.of_evar_map clenv.evd in
+	let Sigma (evar, evd, _) = new_evar (cl_env clenv) evd ~src ty in
+	let evd = Sigma.to_evar_map evd in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
 	fold clenv mvs in
   fold clenv dep_mvs
@@ -614,7 +617,9 @@ let make_evar_clause env sigma ?len t =
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
       let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let sigma, ev = new_evar ~store env sigma t1 in
+      let sigma = Sigma.Unsafe.of_evar_map sigma in
+      let Sigma (ev, sigma, _) = new_evar ~store env sigma t1 in
+      let sigma = Sigma.to_evar_map sigma in
       let dep = dependent (mkRel 1) t2 in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f549913f2..bc2cc3e91 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -65,7 +65,9 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
+    let sigma = Sigma.Unsafe.of_evar_map sigma in
+    let Sigma (econstr, sigma, _) = Evarutil.new_evar env sigma ~src ~store typ in
+    let sigma = Sigma.to_evar_map sigma in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index c3fe6b657..3d544274d 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 1b6ba56e6..7e0182137 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 90e4f8521..8a8b36a9e 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