From e69f8622d1b844f77d14e3ba4db797f7c64e6bed Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Sun, 29 Jan 2017 18:42:33 +0100
Subject: 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).
---
 toplevel/vernacentries.ml | 3 ---
 1 file changed, 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. *)
-- 
cgit v1.2.3