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
---
 tactics/tacinterp.ml | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9ce5cbf328..cd494a3e15 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -984,10 +984,7 @@ let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
 let pack_sigma (sigma,c) = {it=c;sigma=sigma}
 
 let extend_gl_hyps { it=gl ; sigma=sigma } sign =
-  let hyps = Goal.V82.hyps sigma gl in
-  let new_hyps = List.fold_right Environ.push_named_context_val sign hyps in
-  (* spiwack: (2010/01/13) if a bug was reintroduced in [change] in is probably here *)
-  Goal.V82.new_goal_with sigma gl new_hyps
+  Goal.V82.new_goal_with sigma gl sign
 
 (* Interprets an l-tac expression into a value *)
 let rec val_interp ist gl (tac:glob_tactic_expr) =
-- 
cgit v1.2.3