diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
| commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
| tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /library/global.ml | |
| parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) | |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 19 |
1 files changed, 10 insertions, 9 deletions
diff --git a/library/global.ml b/library/global.ml index 8694d7af..b4d3a7ff 100644 --- a/library/global.ml +++ b/library/global.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: global.ml,v 1.43.2.2 2005/11/23 14:46:17 barras Exp $ *) +(* $Id: global.ml 7639 2005-12-02 10:01:15Z gregoire $ *) open Util open Names @@ -39,6 +39,7 @@ let _ = let universes () = universes (env()) let named_context () = named_context (env()) +let named_context_val () = named_context_val (env()) let push_named_assum a = let (cst,env) = push_named_assum a !global_env in @@ -134,14 +135,14 @@ let env_of_context hyps = open Libnames let type_of_reference env = function - | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t + | VarRef id -> Environ.named_type id env | ConstRef c -> Environ.constant_type env c - | IndRef ind -> Inductive.type_of_inductive env ind - | ConstructRef cstr -> Inductive.type_of_constructor env cstr + | IndRef ind -> + let specif = Inductive.lookup_mind_specif env ind in + Inductive.type_of_inductive specif + | ConstructRef cstr -> + let specif = + Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in + Inductive.type_of_constructor cstr specif let type_of_global t = type_of_reference (env ()) t - - -(*let get_kn dp l = - make_kn (current_modpath !global_env) dp l -*) |