• Jean-Christophe Filliatre's avatar
    Coq output: recursive definitions · 59b180cb
    Jean-Christophe Filliatre authored
    introduced new transformation eliminate_non_struct_recursion for that purpose
    uses Decl.check_termination tomake the check and the pretty-print
    (could probably be improved to avoid 3 calls to check_termination)
    59b180cb
Name
Last commit
Last update
..
bench Loading commit data...
config Loading commit data...
coq-plugin Loading commit data...
core Loading commit data...
driver Loading commit data...
ide Loading commit data...
parser Loading commit data...
printer Loading commit data...
programs Loading commit data...
tools Loading commit data...
tptp2why Loading commit data...
transform Loading commit data...
util Loading commit data...
why3doc Loading commit data...
config.sh.in Loading commit data...
main.ml Loading commit data...
why3.ml Loading commit data...