• Julien Thierry's avatar
    Minor fix in Coq printer. · 9c0d73ef
    Julien Thierry authored
    When the proof terminator was missing at the end of a Coq file, Why3
    deleted the whole proof. Now Why3 no longer discards the proof
    inadvertently.
    9c0d73ef
coq.ml 34.2 KB