diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-10 15:45:38 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-10 15:45:38 +0000 |
| commit | 8a78cc1f4cc51423a5eccfd2d07a2133a84f670b (patch) | |
| tree | 588526025df0f9d481555890411d0124538aff96 /pretyping/termops.ml | |
| 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
Diffstat (limited to 'pretyping/termops.ml')
0 files changed, 0 insertions, 0 deletions