Making Evarutil.new_evar monotonous.

4 files changed, 32 insertions, 19 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d5bb564f66..60d92f4beb 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 1c3ae9ad95..bc9f083315 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 76d67c748d..96648bb111 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 123f9b8cd3..9caa868958 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