diff options
| author |  aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-18 14:47:43 +0000 |
|---|---|---|
| committer | aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-04-18 14:47:43 +0000 |
| commit | a5c1b866a6d7f096d6fcb30bd63036436cfd36f8 (patch) | |
| tree | 2e1b419d0707e3ae501a7461f53f490568531577 /toplevel/vernacentries.ml | |
| 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 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 538a502ec..3652e2a6b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -355,7 +355,7 @@ let vernac_definition (local,k) (loc,id as lid) def hook = | None -> None | Some r -> let (evc,env)= get_current_context () in - Some (interp_redexp env evc r) in + Some (snd (interp_redexp env evc r)) in do_definition id (local,k) bl red_option c typ_opt hook) let vernac_start_proof kind l lettop hook = @@ -1205,13 +1205,14 @@ let vernac_check_may_eval redexp glopt rc = if !pcoq <> None then (Option.get !pcoq).print_check env j else msg (print_judgment env j) | Some r -> - let redfun = fst (reduction_of_red_expr (interp_redexp env sigma' r)) in + let (sigma',r_interp) = interp_redexp env sigma' r in + let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None then (Option.get !pcoq).print_eval redfun env sigma' rc j else msg (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = - declare_red_expr locality s (interp_redexp (Global.env()) Evd.empty r) + declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r)) (* The same but avoiding the current goal context if any *) let vernac_global_check c = |