From fc6496dcc326852533ea4d860cdea85c6ee79b3b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Jan 2013 18:15:10 +0000
Subject: Fixed synchronicity of filter with evar context in new_goal_with.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16173 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/cc/ccalgo.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index a85c80a79e..c8238804a0 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -727,9 +727,7 @@ let __eps__ = Id.of_string "_eps_"
 let new_state_var typ state =
   let id = pf_get_new_id __eps__ state.gls in
   let {it=gl ; sigma=sigma} = state.gls in
-  let new_hyps =
-    Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in
-  let gls = Goal.V82.new_goal_with sigma gl new_hyps in
+  let gls = Goal.V82.new_goal_with sigma gl [id,None,typ] in
     state.gls<- gls;
     id
 
-- 
cgit v1.2.3