From 8eea39501acffa5f7a4ea046ff3862e391d0655c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 28 Sep 2017 22:43:39 +0200
Subject: Remove trivial TODO comment (constants can't be template poly now).

---
 pretyping/retyping.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'pretyping/retyping.ml')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 079524f34..56f8b33e0 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -214,7 +214,6 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
           type_of_inductive_knowing_conclusion env sigma (spec, EInstance.kind sigma u) conclty
     | Const (cst, u) ->
         let t = constant_type_in env (cst, EInstance.kind sigma u) in
-        (* TODO *)
           sigma, EConstr.of_constr t
     | Var id -> sigma, type_of_var env id
     | Construct (cstr, u) -> sigma, EConstr.of_constr (type_of_constructor env (cstr, EInstance.kind sigma u))
-- 
cgit v1.2.3