diff options
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 8b7d654572..3afe04b37b 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -517,9 +517,6 @@ let vernac_end_proof ?proof = function | Admitted -> save_proof ?proof Admitted | Proved (_,_) as e -> 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. *) |