Ssreflect Users Discussion List

[<>]

Dear Assia,

thank you for the reply.

I want to use this facility for painlessly debugging my tactics
by compacting the context; I am afraid I can not exploit your suggestion.

More details:
I am developing a tactic library which performs, in brief, 
symbolic evaluation for a language with the axiomatic semantics.
The tactics work by pattern matching to decide what to evaluate,
assuming all abbreviations are unfolded. 

The problem is that the tactics may fail, because there are bugs in the 
tactics
or there is not sufficient information in the context for 
symbolic evaluation to succeed. In either case, the tactics leave
traces of what they have successfully evaluated, as facts in the context.
Let me note that since traces are produced by the tactics, abbreviations are
unfolded and there is no way to fold them beforehand.
The traces blow up the context and I usually get dazzled. 

This is where I want to benefit from the facility I asked;
debugging is a substantial part of the development. 

Best regards,
Keiko