diff options
| author | msozeau | 2011-03-10 15:45:38 +0000 |
|---|---|---|
| committer | msozeau | 2011-03-10 15:45:38 +0000 |
| commit | 8a78cc1f4cc51423a5eccfd2d07a2133a84f670b (patch) | |
| tree | 588526025df0f9d481555890411d0124538aff96 | |
| parent | 1ac63f8e8cdc66b117a9b0deab1ab7a8afba41df (diff) | |
Do not forget conv_pbs when resetting an evm:
- In clenv, this used to forget the existing constraints, there are none
in the other evar_map.
- Other uses (evar_refiner, class_tactics) always reset with an enriched
version of the same evar_map.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13901 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/evd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 36abd54061..706a93527c 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -414,7 +414,7 @@ let empty = { metas=Metamap.empty } -let evars_reset_evd evd d = {d with evars = evd.evars} +let evars_reset_evd evd d = {d with evars = evd.evars; conv_pbs = evd.conv_pbs} let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (EvarMap.find d.evars evk).evar_source |