GitLab

I think it is currently passed into the command.

There are still goals that are not printed and callback function must be
better written.
'b' to 't'
't' to 'c'
Needs testing.

at the end of line.
This was commited as a proof of concept. Giving the name at the end is not
convenient.
Should also solve the problem of renaming by asking args_wrapper to do the
work of unification of name.

hypothesis as argument.

+ add type trans_with_args_l + wrap_l + register_..._l
+ add use_th transformation that will use import a theory in the current goal

+ some cleaning / fixes

Added proof_state and functions to control it in controller_itp.
Tried to add a test case for it inside the command p to put a big
P next to a goal that is proved.
It is currently buggy. Needs investigating and cleaning.

Struggling with names. Removed the print_task which looked at the driver
before printing for uniformity. If I dont do that the printing function
I use to have a safe naming environnment inside tasks are not the same
as the printing function we use for display. So hypothesis displayed dont
actually exists and other bugs.

I will try to see if my changes (in particular clean_environnment and
gen_ident) are necessary.

Modifications in Pretty to get real unique names for hypothesis.

I think we need LIFO and not FIFO.

or not before parsing with wrap. So we give a Tformula instead of Tterm
constructor for those transformations.

+ modify the command that print the sessino tree to specify where we are in the tree with "**"
+ add some more comprehensible error messages to wraper function for parsing

"parsing" of these strings is delayed in the transformations themselves,
because in case such an argument must be interpreted as a term, the
task itself is needed do perform name resolution.

Incidentally, saving transformations with arguments in sessions is not an
issue anymore

Only works with hypothesis of the form forall x. A -> B.
Also cleaning the code a little.