• 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
..
jessie Loading commit data...
test-and.why Loading commit data...
test-bobot.why Loading commit data...
test-claude.why Loading commit data...
test-gappa.why Loading commit data...
test-jcf.why Loading commit data...
test-pgm-jcf.mlw Loading commit data...