GitLab

Possibility to add env to transformation via args_wrapper (ugly).

Rewrite and replace.

Seemed useful because the declaration might not be displayed.

On some examples, goal was cut when first end was encountered.

- add session directory and restore old session file mechanism

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.