From 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 15 Feb 2016 13:31:54 +0100
Subject: Renaming functions in Typing to stick to the standard e_* scheme.

---
 proofs/proofview.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'proofs')

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) =
-- 
cgit v1.2.3