diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 09:57:50 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-10-24 10:05:03 +0200 |
| commit | 3df7e2a89ae931207781c6f5cbc9e196235b1dc3 (patch) | |
| tree | 7747e567b36ce6db92154eaeedbe95eaa723c751 /kernel/mod_typing.mli | |
| parent | d30a7244b52e86c364320a8fa0794c7686f30074 (diff) | |
Backtracking on interpreting toplevel calls to exact in scope determined
by the type to prove (was introduced in 35846ec22, r15978, Nov 2012).
Not only it does not work when exact is called via a Ltac definition,
but, also, it does not scale easily to refine which is a TACTIC
EXTEND.
Ideally, one may then want to propagate scope interpretations through
ltac variables, as well as supporting refine...
See #4034 for a discussion.
Diffstat (limited to 'kernel/mod_typing.mli')
0 files changed, 0 insertions, 0 deletions