Commit ee535a72 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Discard old pieces between Qed and the next blank line, so that generated...

Discard old pieces between Qed and the next blank line, so that generated commands about implicit arguments are not preserved.
parent f7abbc29
...@@ -462,7 +462,8 @@ let read_old_script = ...@@ -462,7 +462,8 @@ let read_old_script =
if Str.string_match axm s 0 then if Str.string_match axm s 0 then
(let name = Str.matched_group 2 s in sc := Axiom name :: !sc; (let name = Str.matched_group 2 s in sc := Axiom name :: !sc;
skip_to_empty := true) else skip_to_empty := true) else
if s = "(* Why3 goal *)" then sc := read_old_proof ch :: !sc else if s = "(* Why3 goal *)" then
(sc := read_old_proof ch :: !sc; skip_to_empty := true) else
if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then if s = "(* YOU MAY EDIT THE CONTEXT BELOW *)" then
(sc := read_deprecated_script ch true; raise End_of_file) else (sc := read_deprecated_script ch true; raise End_of_file) else
if s = "(* YOU MAY EDIT THE PROOF BELOW *)" then if s = "(* YOU MAY EDIT THE PROOF BELOW *)" then
......
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