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

4 files changed, 8 insertions, 8 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 09d9cf019..bea449c31 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 f47b35541..47d8eeca2 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 1dd53a3fd..27daa7e3c 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 e203b9f65..ed6db90d6 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 =