Deprecate Typing.e_* functions

15 files changed, 58 insertions, 60 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 =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index ea8557b18..c9c2445a7 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -197,7 +197,8 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
 	  let term = co x in
-	    Typing.e_solve_evars env evdref term)
+          let sigma, term = Typing.solve_evars env !evdref term in
+          evdref := sigma; term)
       in
 	if isEvar !evdref c || isEvar !evdref c' || not (Program.is_program_generalized_coercion ()) then
 	  (* Second-order unification needed. *)
@@ -343,8 +344,9 @@ let app_coercion env evdref coercion v =
   match coercion with
   | None -> v
   | Some f ->
-     let v' = Typing.e_solve_evars env evdref (f v) in
-     whd_betaiota !evdref v'
+    let sigma, v' = Typing.solve_evars env !evdref (f v) in
+    evdref := sigma;
+    whd_betaiota !evdref v'
 
 let coerce_itf ?loc env evd v t c1 =
   let evdref = ref evd in
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index da05102f2..3cf43ace0 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -26,14 +26,17 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
 (** Variant of [type_of] using references instead of state-passing. *)
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
+[@@ocaml.deprecated "Use [Typing.type_of]"]
 
 (** Typecheck a type and return its sort *)
 val sort_of : env -> evar_map -> types -> evar_map * Sorts.t
 val e_sort_of : env -> evar_map ref -> types -> Sorts.t
+[@@ocaml.deprecated "Use [Typing.sort_of]"]
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
 val check : env -> evar_map -> constr -> types -> evar_map
 val e_check   : env -> evar_map ref -> constr -> types -> unit
+[@@ocaml.deprecated "Use [Typing.check]"]
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
@@ -41,6 +44,7 @@ val meta_type : evar_map -> metavariable -> types
 (** Solve existential variables using typing *)
 val solve_evars : env -> evar_map -> constr -> evar_map * constr
 val e_solve_evars : env -> evar_map ref -> constr -> constr
+[@@ocaml.deprecated "Use [Typing.solve_evars]"]
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 5a2d82977..b64e7a2e5 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -30,26 +30,19 @@ let typecheck_evar ev env sigma =
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
     let t = NamedDecl.get_type decl in
-    let evdref = ref sigma in
-    let _ = Typing.e_sort_of env evdref t in
-    let () = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+    let sigma, _ = Typing.sort_of env sigma t in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,body,_) -> Typing.check env sigma body t
     in
-    (!evdref, EConstr.push_named decl env)
+    (sigma, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
   let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
-  let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
-  !evdref
-
-let typecheck_proof c concl env sigma =
-  let evdref = ref sigma in
-  let () = Typing.e_check env evdref c concl in
-  !evdref
+  let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+  sigma
 
 let (pr_constrv,pr_constr) =
   Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
@@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl =
   let fold accu ev = typecheck_evar ev env accu in
   let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
   (** Check that the refined term is typesafe *)
-  let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+  let sigma = if typecheck then Typing.check env sigma c concl else sigma in
   (** Check that the goal itself does not appear in the refined term *)
   let self = Proofview.Goal.goal gl in
   let _ =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 60070e6fe..01351e249 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1985,24 +1985,22 @@ let on_the_bodies = function
 exception DependsOnBody of Id.t option
 
 let check_is_type env sigma ty =
-  let evdref = ref sigma in
   try
-    let _ = Typing.e_sort_of env evdref ty in
-    !evdref
+    let sigma, _ = Typing.sort_of env sigma ty in
+    sigma
   with e when CErrors.noncritical e ->
     raise (DependsOnBody None)
 
 let check_decl env sigma decl =
   let open Context.Named.Declaration in
   let ty = NamedDecl.get_type decl in
-  let evdref = ref sigma in
   try
-    let _ = Typing.e_sort_of env evdref ty in
-    let _ = match decl with
-    | LocalAssum _ -> ()
-    | LocalDef (_,c,_) -> Typing.e_check env evdref c ty
+    let sigma, _ = Typing.sort_of env sigma ty in
+    let sigma = match decl with
+    | LocalAssum _ -> sigma
+    | LocalDef (_,c,_) -> Typing.check env sigma c ty
     in
-    !evdref
+    sigma
   with e when CErrors.noncritical e ->
     let id = NamedDecl.get_id decl in
     raise (DependsOnBody (Some id))
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 7b382dacc..85c0699ea 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -199,9 +199,7 @@ let interp_recursive ~program_mode ~cofix fixl notations =
              try
                let sigma, h_term = fix_proto sigma in
                let app = mkApp (h_term, [|sort; t|]) in
-               let _evd = ref sigma in
-               let res = Typing.e_solve_evars env _evd app in
-               !_evd, res
+               Typing.solve_evars env sigma app
              with e when CErrors.noncritical e -> sigma, t
            in
            sigma, LocalAssum (id,fixprot) :: env'
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 745f1df1d..349fc562b 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -190,9 +190,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
         ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
     sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
   in
-  let _evd = ref sigma in
-  let def = Typing.e_solve_evars env _evd def in
-  let sigma = !_evd in
+  let sigma, def = Typing.solve_evars env sigma def in
   let sigma = Evarutil.nf_evar_map sigma in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context sigma binders_rel in