diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:43:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-28 22:43:39 +0200 |
| commit | 8eea39501acffa5f7a4ea046ff3862e391d0655c (patch) | |
| tree | 38ece0503c1609d4c57d32f4e43ec5fa89e746f5 /pretyping/retyping.ml | |
| parent | b9740771e8113cb9e607793887be7a12587d0326 (diff) | |
Remove trivial TODO comment (constants can't be template poly now).
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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)) |