GitLab

This permits using them in transformations, as they also
preserve the term structure.

Export Term.t_ty_map and Term.t_app_map. We can generalize
t_s_map to cover t_app_map, but this requires computing the
list of types for every application, which we rarely need.

which gives us a cheap test for recursive defitions.
We could also make an effort to ignore the conclusions
in inductive predicate definitions but it's probably
not worth it.

(sorry for not doing it earlier)

also, export Ty.ty_v_* traversal functions

thanks to Frédéric Herbreteau for the patch!

The TPTP plugin does not load (Linux 64bit) when compiled with
the Menhir library. For the moment, let us leave it as it is.
The use of the library is not necessary and is off by default.

another birthday gift for François

- in particular, we simplify function definitions before testing
them for linearity (this allows to inline array updates which are
defined via a record update {| a with map = a.map[i <- v] |}).
We really need to add some memoization here, otherwise we might
pay too much.

no more need for 'globals' field in effects