remove_list [H1,H2] works. Without spaces and with this exact syntax.
This is to be modified later. In particular, we should probably handle
parsing of arguments differently.

Destruct_alg that works on polymorphic types.

Adding a forgeting function for printing variables on exceptions.
Should do the same at least for patterns.
Adding printing functions from why3printer.
Changing exception in transformation so that they
return terms not strings.

add a wrap_and_register that ... wraps and registers ! and also add the transformation type to its description

Not yet registered.

I added an exception to TSfailed. Also changed the query exceptions.

Replaced one by 1 in induction.

Also, added a debug flag to be raised when matching of apply fail.
To do that, I changed exception NoMatch so that it returns the terms
that cant be matched.
This needs some testing.

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

Rewrite and replace.

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

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.