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

4 files changed, 12 insertions, 11 deletions

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
 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index df3f6e0dbd..1a7e9a9830 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -554,10 +554,16 @@ module V82 = struct
        with a good implementation of them.
     *)
 
-  (* Used for congruence closure *)
-  let new_goal_with sigma gl new_hyps =
+  (* Used for congruence closure and change *)
+  let new_goal_with sigma gl extra_hyps =
     let evi = content sigma gl in
-    let new_evi = { evi with Evd.evar_hyps = new_hyps } in
+    let hyps = evi.Evd.evar_hyps in
+    let new_hyps =
+      List.fold_right Environ.push_named_context_val extra_hyps hyps in
+    let extra_filter = List.map (fun _ -> true) extra_hyps in
+    let new_filter = extra_filter @ evi.Evd.evar_filter in
+    let new_evi =
+      { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
     let evk = Evarutil.new_untyped_evar () in
     let new_sigma = Evd.add Evd.empty evk new_evi in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 1146d95f61..72f1b16a46 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -232,7 +232,7 @@ module V82 : sig
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
  (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal ->  Environ.named_context_val -> goal Evd.sigma 
+  val new_goal_with : Evd.evar_map -> goal -> Sign.named_context -> goal Evd.sigma
 
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map
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) =