GitLab

fixes issue #57

a new theory relations.WellFounded is introduced for this purpose
(and must be imported whenever one wants to make use of a custom
relation for a variant)

it defines, inductively, a notion of accessibility for a given
predicate R (x is accessible whenever all elements smaller than x for R
are alreay accessible)

whenever one has to prove that a variant decreases, a new VC is also
generated, to show that the old value of the variant is accessible
for the order relation

note: accessibility being defined inductively, proving well-foundedness
is out of reach of SMT solvers; but at least this is sound now

Also, move some model-related labelling from Parser to Vc.

a branch is typed *after* unifying the type of the pattern with the
type of the matched value

fixes issue #124 (return type and coercions)

done in both logic and programs

Compile support for provers is now checked only when the version matches
or when going through the unrecognized provers. This commit also improves
the output, since the "detected provers" were only the ones added to the
configuration file, not the ones actually detected (e.g. bad versions,
empty commands, missing support).

This makes it more consistent with the [@...] syntax for generic tags.