From c0e99b45a97aa0d506e32d1daeb594c372ea82fa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Feb 2018 21:39:49 +0100
Subject: [vernac] Fix outdated comment.

---
 vernac/vernacentries.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e19ca2b6b8..35ef4bfa45 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2279,8 +2279,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
   then Flags.verbosely control c
   else control  c
 
-(* XXX: There is a bug here in case of an exception, see @gares
-   comments on the PR *)
+(* Be careful with the cache here in case of an exception. *)
 let interp ?verbosely ?proof ~st cmd =
   Vernacstate.unfreeze_interp_state st;
   try
-- 
cgit v1.2.3