From 9369925f8edebf18a7d9cc9516521f193117f3f8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 13 Apr 2011 14:28:32 +0000
Subject: - Remove create_evar_defs - Be careful with
 consider_remaining_unif_problems: it might instantiate an evar, including the
 current goal!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13995 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 52765ff12d..9a599c8ab8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1524,7 +1524,7 @@ let interp_open_constr sigma env c =
 
 let interp_open_constr_patvar sigma env c =
   let raw = intern_gen false sigma env c ~allow_patvar:true in
-  let sigma = ref (Evd.create_evar_defs sigma) in
+  let sigma = ref sigma in
   let evars = ref (Gmap.empty : (identifier,glob_constr) Gmap.t) in
   let rec patvar_to_evar r = match r with
     | GPatVar (loc,(_,id)) ->
-- 
cgit v1.2.3