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 /test-suite | |
| 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 'test-suite')
0 files changed, 0 insertions, 0 deletions