diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 10:23:28 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-09-04 15:22:27 +0200 |
| commit | 3806d567af6b1feee2c8f196199eee4208a8551d (patch) | |
| tree | 5e6a7657058d52f18869c3bdfa618e5f7bb26b90 /tactics | |
| parent | f3b714f5a8e516ee9731d705808a4084caae5a1e (diff) | |
Typing.sort_of does not leak evarmaps anymore.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/rewrite.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 [||] |