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.

---
 tactics/rewrite.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index b67aee7f77..5c2e3ec293 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 [||]
-- 
cgit v1.2.3