diff options
| author | Théo Zimmermann | 2017-01-29 18:42:33 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2017-01-29 18:42:33 +0100 |
| commit | e69f8622d1b844f77d14e3ba4db797f7c64e6bed (patch) | |
| tree | df474c2cb991e41ee9a45f1125a15d16c17f180c | |
| parent | c7a0568967a8a6e40888a2106b9b59325f2f09a5 (diff) | |
Remove outdated comment from 2002.
The comment was arguing against the "Proof proof_term." syntax.
This syntax is still there 15 years later (while the alternative
proposition uses outdated syntax).
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a2f2ded327..e5e2c6179c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -521,9 +521,6 @@ let vernac_end_proof ?proof = function Stm.show_script ?proof (); save_proof ?proof e - (* A stupid macro that should be replaced by ``Exact c. Save.'' all along - the theories [??] *) - let vernac_exact_proof c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is called only at the begining of a proof. *) |