diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:35:07 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:11 +0200 |
| commit | 91b1808056602f3e26d1eb1bdf7be1e791cb742d (patch) | |
| tree | 3bdb404bb7b88d8a993c326c4712dfcacaf73d17 /tactics/autorewrite.ml | |
| parent | 02aace9f038d579e9cf32dc2f5b21d415e977c03 (diff) | |
Univs: fix many evar_map initializations and leaks.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 2b3fadf7f..3a9d40de0 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -292,10 +292,13 @@ let find_applied_relation metas loc env sigma c left2right = (* To add rewriting rules to a base *) let add_rew_rules base lrul = let counter = ref 0 in + let env = Global.env () in + let sigma = Evd.from_env env in let lrul = List.fold_left (fun dn (loc,(c,ctx),b,t) -> - let info = find_applied_relation false loc (Global.env ()) Evd.empty c b in + let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in + let info = find_applied_relation false loc env sigma c b in let pat = if b then info.hyp_left else info.hyp_right in let rul = { rew_lemma = c; rew_type = info.hyp_ty; rew_pat = pat; rew_ctx = ctx; rew_l2r = b; |