diff options
| -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. *) |