diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-28 20:17:37 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-12-28 20:17:37 +0000 |
| commit | 3aa64a257dfc3854b30f4655c6a64c25108ec8e1 (patch) | |
| tree | 7ed632108dc44d31a32f2ec7b0c56c8dcc7a1aab /tactics/equality.mli | |
| parent | 42ea537affb88f8e63499d909eb526e024fc0aec (diff) | |
Safer, though ad hoc, approach to re-interpretation of the argument of
general_multi_multi_rewrite. Due to the option "!" of rewrite, a lemma
may need to be interpreted several times with different instances of
the implicit arguments. Interpreting the term as a constr in
tacinterp.ml would need to either refresh the holes (i.e. the evars)
or detype what has been typed and in both cases, complicated things
can happen because the evars associated to these holes may have been
used in instantiating former evars of the goal. Leaving the term as a
rawconstr would need to export the interpretation functions from
tacinterp which is technically complicated in the current situation
because equality.ml is currently linked before tacinterp. The solution
used is to delay the interpretation using an ML closure.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12610 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
| -rw-r--r-- | tactics/equality.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli index 9986d230b..b5c147393 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -68,9 +68,13 @@ val general_rewrite_in : val general_multi_rewrite : orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic + +type delayed_open_constr_with_bindings = + env -> evar_map -> evar_map * constr with_bindings + val general_multi_multi_rewrite : - evars_flag -> (bool * multi * constr with_bindings sigma) list -> clause -> - (tactic * conditions) option -> tactic + evars_flag -> (bool * multi * delayed_open_constr_with_bindings) list -> + clause -> (tactic * conditions) option -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic val replace : constr -> constr -> tactic |