diff options
| author | Pierre-Marie Pédrot | 2016-03-28 16:07:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-28 16:15:35 +0200 |
| commit | 59586ce49266f6b709cb53e4647b8907a7a08eb8 (patch) | |
| tree | 55df78fa09331e7fc1e02dd9bcd43e8dfdcff33d | |
| parent | 111e5edfe388d2f41ddef11800dac55b060b280b (diff) | |
Fixing an evar leak in Rewrite introduced by 968dfdb15.
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 2fe2eb42a6..20d4651efa 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -359,7 +359,7 @@ end) = struct let env' = Environ.push_rel_context rels env in let sigma = Sigma.Unsafe.of_evar_map sigma in let Sigma ((evar, _), evars, _) = Evarutil.new_type_evar env' sigma Evd.univ_flexible in - let evars = Sigma.to_evar_map sigma in + let evars = Sigma.to_evar_map evars in let evars, inst = app_poly env (evars,Evar.Set.empty) rewrite_relation_class [| evar; mkApp (c, params) |] in |