diff options
| author | herbelin | 2013-01-29 18:15:10 +0000 |
|---|---|---|
| committer | herbelin | 2013-01-29 18:15:10 +0000 |
| commit | fc6496dcc326852533ea4d860cdea85c6ee79b3b (patch) | |
| tree | 68c088e4fb6bc21ea2c1f19dffc5aa4de9d8a898 /tactics | |
| parent | 4929fa8a5b65bd90207f3a943227ed09a7ed0b6c (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 5 |
1 files changed, 1 insertions, 4 deletions
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) = |