From 8a78cc1f4cc51423a5eccfd2d07a2133a84f670b Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 10 Mar 2011 15:45:38 +0000
Subject: 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
---
 pretyping/evd.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
 
-- 
cgit v1.2.3