diff options
| author | aspiwack | 2012-04-18 14:47:43 +0000 |
|---|---|---|
| committer | aspiwack | 2012-04-18 14:47:43 +0000 |
| commit | a5c1b866a6d7f096d6fcb30bd63036436cfd36f8 (patch) | |
| tree | 2e1b419d0707e3ae501a7461f53f490568531577 /parsing | |
| parent | 676f63e7b5e0803cf7bee756369323b4ea42052b (diff) | |
Corrects a (very) longstanding bug of tactics. As is were, tactic expecting
constr as argument (rather than openconstr) assumed that the evar_map
output by pretyping was irrelevant as the final constr didn't have any evars.
However, if said constr was defined using pre-existing evars from the
context, the evars may be instantiated by pretyping, hence dropping the
output evar_map led to inconsistent proof terms.
This fixes bug #2739 ( https://coq.inria.fr/bugs/show_bug.cgi?id=2739 ).
Thanks Arthur for noticing it.
Note: change still has the bug, because more serious issues interfered with
my fix.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/argextend.ml4 | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4 index ac5aef8d42..b6fd95a815 100644 --- a/parsing/argextend.ml4 +++ b/parsing/argextend.ml4 @@ -202,9 +202,11 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = let interp = match f with | None -> <:expr< fun ist gl x -> - out_gen $make_wit loc globtyp$ - (Tacinterp.interp_genarg ist gl - (Genarg.in_gen $make_globwit loc globtyp$ x)) >> + let (sigma,a_interp) = + Tacinterp.interp_genarg ist gl + (Genarg.in_gen $make_globwit loc globtyp$ x) + in + (sigma , out_gen $make_wit loc globtyp$ a_interp)>> | Some f -> <:expr< $lid:f$>> in let substitute = match h with | None -> @@ -230,7 +232,8 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl = ((fun e x -> (Genarg.in_gen $globwit$ ($glob$ e (out_gen $rawwit$ x)))), (fun ist gl x -> - (Genarg.in_gen $wit$ ($interp$ ist gl (out_gen $globwit$ x)))), + let (sigma,a_interp) = $interp$ ist gl (out_gen $globwit$ x) in + (sigma , Genarg.in_gen $wit$ a_interp)), (fun subst x -> (Genarg.in_gen $globwit$ ($substitute$ subst (out_gen $globwit$ x))))); Compat.maybe_uncurry (Pcoq.Gram.extend ($lid:s$ : Pcoq.Gram.entry 'a)) |