From dfb5897b99cd21934c5d096c329585367665b986 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 29 Jul 2014 11:04:52 +0200
Subject: Clean up obsolete comment.

---
 tactics/tacinterp.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 9fd1b1c826..b83775b93a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1104,8 +1104,6 @@ and interp_tacarg ist arg : typed_generic_argument GTac.t =
       interp_external loc ist com req la_interp
   | TacFreshId l ->
       GTac.raw_enter begin fun gl ->
-      (* spiwack: I'm probably being over-conservative here,
-         pf_interp_fresh_id shouldn't raise exceptions *)
         let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in
         GTac.return (in_gen (topwit wit_intro_pattern) (dloc, IntroIdentifier id))
       end
-- 
cgit v1.2.3