Typing.sort_of does not leak evarmaps anymore.

6 files changed, 10 insertions, 9 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 1383d8603..e828345fa 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -45,7 +45,8 @@ let whd_delta env=
 
 (* decompose member of equality in an applicative format *)
 
-let sf_of env sigma c = family_of_sort (sort_of env sigma c)
+(** FIXME: evar leak *)
+let sf_of env sigma c = family_of_sort (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 5e915228e..8f20cea6b 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -378,7 +378,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 evd concl) in
+  let sort = family_of_sort (Typing.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 ->
@@ -386,7 +386,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 evd _A) in
+	let asort = family_of_sort (Typing.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/pretyping/cases.ml b/pretyping/cases.ml
index 737c9fa1b..560289d1e 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 8f5a7e39a..d2fddabdc 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 03e62e006..8700df52a 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
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b67aee7f7..5c2e3ec29 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1379,9 +1379,10 @@ exception RewriteFailure of Pp.std_ppcmds
 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 evars = (sigma, Evar.Set.empty) in
+  let evdref = ref sigma in
+  let sort = Typing.sort_of env evdref concl in
+  let evars = (!evdref, Evar.Set.empty) in
   let evars, cstr =
-    let sort = Typing.sort_of env (goalevars evars) concl in
     let prop, (evars, arrow) = 
       if is_prop_sort sort then true, app_poly_sort true env evars impl [||]
       else false, app_poly_sort false env evars TypeGlobal.arrow [||]