diff options
| author | Maxime Dénès | 2017-03-14 20:28:43 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-03-14 20:28:43 +0100 |
| commit | f463fd3d8af95129935f27a981fcd4a8a6f11f75 (patch) | |
| tree | 48052f098e1e8ab37b6b3aed7d63dbc4f4eddb0b | |
| parent | 93a75d635ac3fb52eed7b39c3c7a8e656f0a81b7 (diff) | |
| parent | e69f8622d1b844f77d14e3ba4db797f7c64e6bed (diff) | |
Merge PR#412: Remove outdated comment from 2002.
| -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. *) |