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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index fd98d54579..045678f0c2 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -111,6 +111,7 @@ let _ = Tacinterp.add_interp_genarg "proof_instr" (Decl_interp.intern_proof_instr e (Genarg.out_gen rawwit_proof_instr x)) end, begin fun ist gl x -> (* declares the interpretation function *) + Tacmach.project gl , Genarg.in_gen wit_proof_instr (interp_proof_instr ist gl (Genarg.out_gen globwit_proof_instr x)) end, |