• Jean-Christophe Filliâtre's avatar
    Coq output: recursive definitions · 59b180cb
    Jean-Christophe Filliâtre 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
coq.drv 4.58 KB