Commit 9c0d73ef authored by Julien Thierry's avatar Julien Thierry Committed by Guillaume Melquiond

Minor fix in Coq printer.

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.
parent 15678f50
...@@ -427,6 +427,12 @@ let read_until re s i ch = ...@@ -427,6 +427,12 @@ let read_until re s i ch =
if not (Str.string_match re s i) then if not (Str.string_match re s i) then
while not (Str.string_match re (input_line ch) 0) do () done while not (Str.string_match re (input_line ch) 0) do () done
let read_until_or_eof re s i ch =
try
read_until re s i ch
with
| End_of_file -> ()
let read_old_proof = let read_old_proof =
let def = Str.regexp "\\(Definition\\|Notation\\|Lemma\\|Theorem\\|Variable\\|Hypothesis\\)[ ]+\\([^ :(.]+\\)" in let def = Str.regexp "\\(Definition\\|Notation\\|Lemma\\|Theorem\\|Variable\\|Hypothesis\\)[ ]+\\([^ :(.]+\\)" in
let def_end = Str.regexp ".*[.]$" in let def_end = Str.regexp ".*[.]$" in
...@@ -452,9 +458,9 @@ let read_old_proof = ...@@ -452,9 +458,9 @@ let read_old_proof =
if Str.string_match old_intros s 0 then begin if Str.string_match old_intros s 0 then begin
read_until old_end s (Str.match_end ()) ch; read_until old_end s (Str.match_end ()) ch;
start := pos_in ch; start := pos_in ch;
read_until qed (input_line ch) 0 ch read_until_or_eof qed (input_line ch) 0 ch
end else end else
read_until qed s 0 ch; read_until_or_eof qed s 0 ch;
Vernacular Vernacular
end in end in
let len = pos_in ch - !start in let len = pos_in ch - !start in
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment