diff options
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 -*) |