diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 16:02:04 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-11-16 16:02:04 +0000 |
| commit | 786dbc4a589442275ab012b36d991c6408e24cef (patch) | |
| tree | dc12f5f11163c5a2b7776c720e1cafc5864672b4 /library/global.ml | |
| parent | b01b06d3a843c97adc6c0a0621b8d681c10fa6fe (diff) | |
dead (and obsolete) code (in comments) removed
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6305 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -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 -*) |