From 3806d567af6b1feee2c8f196199eee4208a8551d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 4 Sep 2014 10:23:28 +0200
Subject: Typing.sort_of does not leak evarmaps anymore.

---
 pretyping/cases.ml   | 2 +-
 pretyping/typing.ml  | 3 +--
 pretyping/typing.mli | 2 +-
 3 files changed, 3 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 737c9fa1b0..560289d1ee 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2337,7 +2337,7 @@ let compile_program_cases loc style (typing_function, evdref) tycon env
 	    let pred = prepare_predicate_from_arsign_tycon loc tomatchs sign t in
 	      (* The tycon may be ill-typed after abstraction. *)
 	    let env' = push_rel_context (context_of_arsign sign) env in
-	      ignore(Typing.sort_of env' !evdref pred); pred
+	      ignore(Typing.sort_of env' evdref pred); pred
 	  with e when Errors.noncritical e ->
 	    let nar = List.fold_left (fun n sign -> List.length sign + n) 0 sign in
 	      lift nar t
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 8f5a7e39a1..d2fddabdca 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -277,8 +277,7 @@ let type_of env evd c =
 
 (* Sort of a type *)
 
-let sort_of env evd c =
-  let evdref = ref evd in
+let sort_of env evdref c =
   let j = execute env evdref c in
   let a = e_type_judgment env evdref j in
   a.utj_type
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 03e62e0060..8700df52a8 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -22,7 +22,7 @@ val type_of : env -> evar_map -> constr -> types
 val e_type_of : ?refresh:bool -> env -> evar_map -> constr -> evar_map * types
 
 (** Typecheck a type and return its sort *)
-val sort_of : env -> evar_map -> types -> sorts
+val 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 -> constr -> types -> unit
-- 
cgit v1.2.3