the verification algorithm must always terminate and be reasonably
performant in practice, but its worst-case complexity is unknown
and probably exponential. What is quite easy when there is only
one recursive definition, becomes difficult when there is a group
of mutually recursive definitions. An educated discussion would
be highly appreciated.

BTW, I had to convert a couple of recursive "logic"s on integers
into an abstract "logic" + axiom. Pretty much all of them supposed
that the argument was non-negative, and thus were non-terminating!

programs: as a side-effect of the new for loop, the syntax 'variant {t} for R' is changed into 'variant {t} with R' (no big deal, it is rarely used)

programs: fixed typing related to exceptions which cannot be raised, or possibly raised but no occuring in post (by the way: how should we issue warning in Why 3?)

configuration file doesn't exists

No commit message