From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 28 Jan 2017 14:11:50 +0100
Subject: Remove useless comments

---
 plugins/extraction/extraction.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 33fab74e13..2b19c2805f 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -258,7 +258,7 @@ let rec extract_type env db j c args =
     | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-        let typ = Typeops.type_of_constant_in env c in (* FIXME constraints *)
+        let typ = Typeops.type_of_constant_in env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
-- 
cgit v1.2.3