Monotonizing the Evarutil module.

Some functions were left in the old paradigm because they are only used by the
unification algorithms, so they are not worthwhile to change for now.

2 files changed, 19 insertions, 12 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 29002af9e0..c50535a17a 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -64,8 +64,10 @@ type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
 
 let find_global dir s =
   let gr = lazy (try_find_global_reference dir s) in
-    fun (evd,cstrs) -> 
-      let evd, c = Evarutil.new_global evd (Lazy.force gr) in
+    fun (evd,cstrs) ->
+      let sigma = Sigma.Unsafe.of_evar_map evd in
+      let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force gr) in
+      let evd = Sigma.to_evar_map sigma in
 	(evd, cstrs), c
 
 (** Utility for dealing with polymorphic applications *)
@@ -172,13 +174,17 @@ end) = struct
   let proper_type = 
     let l = lazy (Lazy.force proper_class).cl_impl in
       fun (evd,cstrs) -> 
-	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+        let sigma = Sigma.Unsafe.of_evar_map evd in
+        let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+        let evd = Sigma.to_evar_map sigma in
 	  (evd, cstrs), c
 	
   let proper_proxy_type = 
     let l = lazy (Lazy.force proper_proxy_class).cl_impl in
       fun (evd,cstrs) -> 
-	let evd, c = Evarutil.new_global evd (Lazy.force l) in
+        let sigma = Sigma.Unsafe.of_evar_map evd in
+        let Sigma (c, sigma, _) = Evarutil.new_global sigma (Lazy.force l) in
+        let evd = Sigma.to_evar_map sigma in
 	  (evd, cstrs), c
 
   let proper_proof env evars carrier relation x =
@@ -347,7 +353,9 @@ end) = struct
 	  (try
 	   let params, args = Array.chop (Array.length args - 2) args in
 	   let env' = Environ.push_rel_context rels env in
-	   let evars, (evar, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+	   let sigma = Sigma.Unsafe.of_evar_map sigma in
+	   let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in
+	   let evars = Sigma.to_evar_map sigma in
 	   let evars, inst = 
 	     app_poly env (evars,Evar.Set.empty)
 	       rewrite_relation_class [| evar; mkApp (c, params) |] in
@@ -407,7 +415,9 @@ module TypeGlobal = struct
 
 
   let inverse env (evd,cstrs) car rel = 
-    let evd, sort = Evarutil.new_Type ~rigid:Evd.univ_flexible env evd in
+    let sigma = Sigma.Unsafe.of_evar_map evd in
+    let Sigma (sort, sigma, _) = Evarutil.new_Type ~rigid:Evd.univ_flexible env sigma in
+    let evd = Sigma.to_evar_map sigma in
       app_poly_check env (evd,cstrs) coq_inverse [| car ; car; sort; rel |]
 
 end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index aeb3726a0c..46e8798543 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -163,14 +163,13 @@ let _ =
     does not check anything. *)
 let unsafe_intro env store (id, c, t) b =
   Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-    let sigma = Sigma.to_evar_map sigma in
     let ctx = named_context_val env in
     let nctx = push_named_context_val (id, c, t) ctx in
     let inst = List.map (fun (id, _, _) -> mkVar id) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar id) b in
-    let sigma, ev = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
-    Sigma.Unsafe.of_pair (mkNamedLambda_or_LetIn (id, c, t) ev, sigma)
+    let Sigma (ev, sigma, p) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    Sigma (mkNamedLambda_or_LetIn (id, c, t) ev, sigma, p)
   end }
 
 let introduction ?(check=true) id =
@@ -344,9 +343,7 @@ let rename_hyp repl =
       let nctx = Environ.val_of_named_context nhyps in
       let instance = List.map (fun (id, _, _) -> mkVar id) hyps in
       Proofview.Refine.refine ~unsafe:true { run = begin fun sigma ->
-        let sigma = Sigma.to_evar_map sigma in
-        let (sigma, c) = Evarutil.new_evar_instance nctx sigma nconcl ~store instance in
-        Sigma.Unsafe.of_pair (c, sigma)
+        Evarutil.new_evar_instance nctx sigma nconcl ~store instance
       end }
     end }