Renaming functions in Typing to stick to the standard e_* scheme.

13 files changed, 29 insertions, 29 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 09d9cf0195..bea449c31a 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -47,7 +47,7 @@ let whd_delta env=
 (* decompose member of equality in an applicative format *)
 
 (** FIXME: evar leak *)
-let sf_of env sigma c = sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) c
 
 let rec decompose_term env sigma t=
     match kind_of_term (whd env t) with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index f47b355417..47d8eeca28 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -404,7 +404,7 @@ let concl_refiner metas body gls =
   let concl = pf_concl gls in
   let evd = sig_sig gls in
   let env = pf_env gls in
-  let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in
+  let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
   let rec aux env avoid subst = function
       [] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
     | (n,typ)::rest ->
@@ -412,7 +412,7 @@ let concl_refiner metas body gls =
 	let x = id_of_name_using_hdchar env _A Anonymous in
 	let _x = fresh_id avoid x gls in
 	let nenv = Environ.push_named (_x,None,_A) env in
-	let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
+	let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
 	let nsubst = (n,mkVar _x)::subst in
 	  if List.is_empty rest then
 	    asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 1dd53a3fd8..27daa7e3c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1170,7 +1170,7 @@ struct
 
     let is_prop term =
      let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
-     let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
+     let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
      Term.is_prop_sort sort in
      
     let rec xparse_formula env tg term =
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e203b9f651..ed6db90d63 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -527,8 +527,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
 	  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.solve_evars env evd setoid in
-	let op_morph = Typing.solve_evars env evd op_morph 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)
     | _ ->
 	let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -627,7 +627,7 @@ let make_hyp_list env evd lH =
       (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
       (plapp evd coq_nil [|carrier|])
   in 
-  let l' = Typing.solve_evars env evd l in
+  let l' = Typing.e_solve_evars env evd l in
     Evarutil.nf_evars_universes !evd l'
 
 let interp_power env evd pow =
@@ -753,7 +753,7 @@ 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.solve_evars env evd l
+  in Typing.e_solve_evars env evd l
 
 let carg = Tacinterp.Value.of_constr
 let tacarg expr =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 489a311bc6..8dae311a9f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -187,7 +187,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		    (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	else Some (fun x -> 
 	  let term = co x in
-	    Typing.solve_evars env evdref term)
+	    Typing.e_solve_evars env evdref term)
       in
 	if isEvar c || isEvar c' then
 	  (* Second-order unification needed. *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index fb0c49320f..022c85340a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -267,7 +267,7 @@ and execute_recdef env evdref (names,lar,vdef) =
 
 and execute_array env evdref = Array.map (execute env evdref)
 
-let check env evdref c t =
+let e_check env evdref c t =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
   if not (Evarconv.e_cumul env evdref j.uj_type t) then
@@ -283,7 +283,7 @@ let unsafe_type_of env evd c =
 
 (* Sort of a type *)
 
-let sort_of env evdref c =
+let e_sort_of env evdref c =
   let env = enrich_env env evdref in
   let j = execute env evdref c in
   let a = e_type_judgment env evdref j in
@@ -310,10 +310,10 @@ let e_type_of ?(refresh=false) env evdref c =
       c
     else j.uj_type
 
-let solve_evars env evdref c =
+let e_solve_evars env evdref c =
   let env = enrich_env env evdref in
   let c = (execute env evdref c).uj_val in
   (* side-effect on evdref *)
   nf_evar !evdref c
 
-let _ = Evarconv.set_solve_evars solve_evars
+let _ = Evarconv.set_solve_evars e_solve_evars
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index dafd75231a..e524edcca8 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -24,16 +24,16 @@ val type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 val e_type_of : ?refresh:bool -> env -> evar_map ref -> constr -> types
 
 (** Typecheck a type and return its sort *)
-val sort_of : env -> evar_map ref -> types -> sorts
+val e_sort_of : env -> evar_map ref -> types -> sorts
 
 (** Typecheck a term has a given type (assuming the type is OK) *)
-val check   : env -> evar_map ref -> constr -> types -> unit
+val e_check   : env -> evar_map ref -> constr -> types -> unit
 
 (** Returns the instantiated type of a metavariable *)
 val meta_type : evar_map -> metavariable -> types
 
 (** Solve existential variables using typing *)
-val solve_evars : env -> evar_map ref -> constr -> constr
+val e_solve_evars : env -> evar_map ref -> constr -> constr
 
 (** Raise an error message if incorrect elimination for this inductive *)
 (** (first constr is term to match, second is return predicate) *)
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 8008b00253..38e9cafad1 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1077,10 +1077,10 @@ struct
     (** Typecheck the hypotheses. *)
     let type_hyp (sigma, env) (na, body, t as decl) =
       let evdref = ref sigma in
-      let _ = Typing.sort_of env evdref t in
+      let _ = Typing.e_sort_of env evdref t in
       let () = match body with
       | None -> ()
-      | Some body -> Typing.check env evdref body t
+      | Some body -> Typing.e_check env evdref body t
       in
       (!evdref, Environ.push_named decl env)
     in
@@ -1089,12 +1089,12 @@ struct
     let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
     (** Typecheck the conclusion *)
     let evdref = ref sigma in
-    let _ = Typing.sort_of env evdref (Evd.evar_concl info) 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.check env evdref c concl in
+    let () = Typing.e_check env evdref c concl in
     !evdref
 
   let (pr_constrv,pr_constr) =
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 97b5ba0cc5..30e157ffd3 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -74,7 +74,7 @@ let let_evar name typ =
     let sigma = Tacmach.New.project gl in
     let env = Proofview.Goal.env gl in
     let sigma = ref sigma in
-    let _ = Typing.sort_of env sigma typ in
+    let _ = Typing.e_sort_of env sigma typ in
     let sigma = Sigma.Unsafe.of_evar_map !sigma in
     let id = match name with
     | Names.Anonymous -> 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c50535a17a..d0a090e5c1 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -107,7 +107,7 @@ 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.solve_evars env evdref (mkApp (fc, args)) in
+  let t = Typing.e_solve_evars env evdref (mkApp (fc, args)) in
     (!evdref, cstrs), t
 
 let app_poly_nocheck env evars f args =
@@ -1452,7 +1452,7 @@ 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 evdref = ref sigma in
-  let sort = Typing.sort_of env evdref concl 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/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1112da4a0d..91711c2f74 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -812,7 +812,7 @@ let interp_may_eval f ist env sigma = function
 	let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in
 	let evdref = ref sigma in
 	let c = subst_meta [Constr_matching.special_meta,ic] ctxt in
-	let c = Typing.solve_evars env evdref c in
+	let c = Typing.e_solve_evars env evdref c in
 	!evdref , c
       with
 	| Not_found ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 46e8798543..f76f4f6e20 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1814,7 +1814,7 @@ let check_is_type env ty msg =
   Proofview.tclEVARMAP >>= fun sigma ->
   let evdref = ref sigma in
   try
-    let _ = Typing.sort_of env evdref ty in
+    let _ = Typing.e_sort_of env evdref ty in
     Proofview.Unsafe.tclEVARS !evdref
   with e when Errors.noncritical e ->
     msg e
@@ -1823,10 +1823,10 @@ let check_decl env (_, c, ty) msg =
   Proofview.tclEVARMAP >>= fun sigma ->
   let evdref = ref sigma in
   try
-    let _ = Typing.sort_of env evdref ty in
+    let _ = Typing.e_sort_of env evdref ty in
     let _ = match c with
     | None -> ()
-    | Some c -> Typing.check env evdref c ty
+    | Some c -> Typing.e_check env evdref c ty
     in
     Proofview.Unsafe.tclEVARS !evdref
   with e when Errors.noncritical e ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 18b2b1444d..b6313cdbab 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1004,7 +1004,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	       ~src:(Loc.ghost, Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
 	     prop |])
   in
-  let def = Typing.solve_evars env evdref def in
+  let def = Typing.e_solve_evars env evdref def in
   let _ = evdref := Evarutil.nf_evar_map !evdref in
   let def = mkApp (def, [|intern_body_lam|]) in
   let binders_rel = nf_evar_context !evdref binders_rel in
@@ -1078,7 +1078,7 @@ let interp_recursive isfix fixl notations =
 	   let fixprot =
 	     try 
 	       let app = mkApp (delayed_force fix_proto, [|sort; t|]) in
-		 Typing.solve_evars env evdref app
+		 Typing.e_solve_evars env evdref app
 	     with e  when Errors.noncritical e -> t
 	   in
 	     (id,None,fixprot) :: env'