Deprecate Typing.e_* functions

9 files changed, 32 insertions, 27 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index c4db49cd3..361981c5b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -49,7 +49,7 @@ let whd_delta env sigma t =
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = e_sort_of env (ref sigma) c
+let sf_of env sigma c = snd (sort_of env sigma c)
 
 let rec decompose_term env sigma t=
     match EConstr.kind sigma (whd env sigma t) with
@@ -264,9 +264,8 @@ let app_global_with_holes f args n =
       let ans = mkApp (fc, args) in
       let (sigma, holes) = gen_holes env sigma t n [] in
       let ans = applist (ans, holes) in
-      let evdref = ref sigma in
-      let () = Typing.e_check env evdref ans concl in
-      (!evdref, ans)
+      let sigma = Typing.check env sigma ans concl in
+      (sigma, ans)
     end
   end
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index a0616b308..44fa0740d 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1051,7 +1051,8 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
       evd:=evd';
-      let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
+      let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd res in
+      evd := sigma;
       res
   in
   let nb_intro_to_do = nb_prod (project g) (pf_concl g) in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 04a23cdb9..dc0f240bd 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -291,7 +291,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let new_princ_name =
     next_ident_away_in_goal (Id.of_string "___________princ_________") Id.Set.empty
   in
-  let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr new_principle_type) in
+  let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
+  evd := sigma;
   let hook = Lemmas.mk_hook (hook new_principle_type) in
   begin
     Lemmas.start_proof
@@ -630,7 +631,8 @@ let build_scheme fas =
 	    in
             let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-            let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in
+            let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd f in
+            evd := sigma;
             let c, u =
               try EConstr.destConst !evd f
               with DestKO ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 7df57b577..efbd029e4 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -385,7 +385,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-             let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
+             let sigma, princ_type = Typing.type_of ~refresh:true env !evd uprinc in
+             evd := sigma;
 	     let princ_type = EConstr.Unsafe.to_constr princ_type in
     	     Functional_principles_types.generate_functional_principle
 	       evd
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 28e85268a..094f54156 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -103,7 +103,8 @@ let generate_type evd g_to_f f graph i =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
   in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let sigma, graph_arity = Typing.type_of (Global.env ()) !evd graph in
+  evd := sigma;
   let ctxt,_ = decompose_prod_assum !evd graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -769,7 +770,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+         let sigma, _ = Typing.type_of (Global.env ()) !evd type_of_lemma in
+         evd := sigma;
 	   let type_of_lemma = nf_zeta type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 9382f567b..fb6be430f 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -85,9 +85,7 @@ let let_evar name typ =
   Proofview.Goal.enter begin fun gl ->
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
-    let sigma = ref sigma in
-    let _ = Typing.e_sort_of env sigma typ in
-    let sigma = !sigma in
+    let sigma, _ = Typing.sort_of env sigma typ in
     let id = match name with
     | Name.Anonymous ->
       let id = Namegen.id_of_name_using_hdchar env sigma typ name in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9eb55aa5e..1b86583da 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -104,9 +104,8 @@ let extends_undefined evars evars' =
 
 let app_poly_check env evars f args =
   let (evars, cstrs), fc = f evars in
-  let evdref = ref evars in 
-  let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
-    (!evdref, cstrs), t
+  let evars, t = Typing.solve_evars env evars (mkApp (fc, args)) in
+  (evars, cstrs), t
 
 let app_poly_nocheck env evars f args =
   let evars, fc = f evars in 
@@ -1469,8 +1468,8 @@ exception RewriteFailure of Pp.t
 type result = (evar_map * constr option * types) option option
 
 let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : result =
+  let sigma, sort = Typing.sort_of env sigma concl in
   let evdref = ref sigma in
-  let sort = Typing.e_sort_of env evdref concl in
   let evars = (!evdref, Evar.Set.empty) in
   let evars, cstr =
     let prop, (evars, arrow) = 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 84049d4ed..a93cf5ae7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -691,11 +691,9 @@ let interp_may_eval f ist env sigma = function
 	let (sigma,ic) = f ist env sigma c in
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let ctxt = EConstr.Unsafe.to_constr ctxt in
-	let evdref = ref sigma in
-	let ic = EConstr.Unsafe.to_constr ic in
+        let ic = EConstr.Unsafe.to_constr ic in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.e_solve_evars env evdref (EConstr.of_constr c) in
-	!evdref , c
+        Typing.solve_evars env sigma (EConstr.of_constr c)
       with
 	| Not_found ->
 	    user_err ?loc ~hdr:"interp_may_eval"
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b2ac3b5a4..074fcb92e 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -505,10 +505,12 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	let op_morph =
 	  match opp with
               Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
-            | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
-	let setoid = Typing.e_solve_evars env evd setoid in
-	let op_morph = Typing.e_solve_evars env evd op_morph in
-	  (setoid,op_morph)
+          | None -> plapp evd coq_eq_smorph [|r;add;mul|] in
+        let sigma = !evd in
+        let sigma, setoid = Typing.solve_evars env sigma setoid in
+        let sigma, op_morph = Typing.solve_evars env sigma op_morph in
+        evd := sigma;
+        (setoid,op_morph)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
 	let signature = [Some (r,Some req);Some (r,Some req)],Some(r,Some req) in
@@ -595,7 +597,8 @@ let make_hyp_list env evdref lH =
       (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
       (plapp evdref coq_nil [|carrier|])
   in 
-  let l' = Typing.e_solve_evars env evdref l in
+  let sigma, l' = Typing.solve_evars env !evdref l in
+  evdref := sigma;
   let l' = EConstr.Unsafe.to_constr l' in
     Evarutil.nf_evars_universes !evdref l'
 
@@ -733,7 +736,9 @@ let make_term_list env evd carrier rl =
   let l = List.fold_right
     (fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
     (plapp evd coq_nil [|carrier|])
-  in Typing.e_solve_evars env evd l
+  in
+  let sigma, l = Typing.solve_evars env !evd l in
+  evd := sigma; l
 
 let carg c = Tacinterp.Value.of_constr (EConstr.of_constr c)
 let tacarg expr =