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 /tactics/tacinterp.mli | |
| 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 'tactics/tacinterp.mli')
| -rw-r--r-- | tactics/tacinterp.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index eff48b100..991fbc88c 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -84,12 +84,12 @@ val add_interp_genarg : string -> (glob_sign -> raw_generic_argument -> glob_generic_argument) * (interp_sign -> goal sigma -> glob_generic_argument -> - typed_generic_argument) * + Evd.evar_map * typed_generic_argument) * (substitution -> glob_generic_argument -> glob_generic_argument) -> unit val interp_genarg : - interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument + interp_sign -> goal sigma -> glob_generic_argument -> Evd.evar_map * typed_generic_argument val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument @@ -117,14 +117,14 @@ val subst_glob_with_bindings : substitution -> glob_constr_and_expr Glob_term.with_bindings -> glob_constr_and_expr Glob_term.with_bindings (** Interprets any expression *) -val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value +val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> Evd.evar_map * value (** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> goal sigma -> glob_tactic_expr -> - constr + Evd.evar_map * constr (** Interprets redexp arguments *) -val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> red_expr +val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr (** Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> identifier list -> @@ -146,7 +146,7 @@ val eval_tactic : glob_tactic_expr -> tactic val interp : raw_tactic_expr -> tactic -val eval_ltac_constr : goal sigma -> raw_tactic_expr -> constr +val eval_ltac_constr : goal sigma -> raw_tactic_expr -> Evd.evar_map * constr val subst_tactic : substitution -> glob_tactic_expr -> glob_tactic_expr |