diff options
| -rw-r--r-- | library/global.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/library/global.ml b/library/global.ml index a1af7c456..9ad01842c 100644 --- a/library/global.ml +++ b/library/global.ml @@ -138,8 +138,3 @@ let type_of_reference env = function | ConstructRef cstr -> Inductive.type_of_constructor env cstr let type_of_global t = type_of_reference (env ()) t - - -(*let get_kn dp l = - make_kn (current_modpath !global_env) dp l -*) |