On Wed, 11 Feb 2015, Dmitriy Traytel wrote:
What remains are slightly odd entry points without context:
resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac. We could
probably remove them altogether, but there are a lot of remaining uses
in the new datatype implementation, which I don't
Hi Makarius,
On 10.02.2015 18:30, Makarius wrote:
On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap
problem for reforms.
I actually did start some work in the vicinity of r
On Tue, 4 Nov 2014, Makarius wrote:
Strange hacks that work around the absence of proper options encumber
the introduction of them eventually. It is the usual bootstrap problem
for reforms.
I actually did start some work in the vicinity of resolve_tac with
proper context recently, but it wi
On Mon, 3 Nov 2014, Peter Lammich wrote:
You can contribute indirectly to important reforms that are in the
pipeline for a long time by keeping your sources in a more up-to-date
state.
As you said, there seems to be no other way of achieving what I
required. I realized that, added a comment
>
> You can contribute indirectly to important reforms that are in the
> pipeline for a long time by keeping your sources in a more up-to-date
> state.
As you said, there seems to be no other way of achieving what I
required. I realized that, added a comment (*Argh!*) expressing my
disgust abo
On Mon, 3 Nov 2014, Peter Lammich wrote:
I have a tactic that has a debug-mode. In debug-mode, it shall output
unification trace for certain (but not all) rule applications.
How to write a tactic
resolve_with_tracing: thm list -> int -> tactic
that behaves like resolve_tac, but outputs unifi
Hi List,
I have a tactic that has a debug-mode. In debug-mode,
it shall output unification trace for certain (but not all) rule
applications.
How to write a tactic
resolve_with_tracing: thm list -> int -> tactic
that behaves like resolve_tac, but outputs unification trace?
Best,
Peter
p
