diff options
| -rw-r--r-- | library/global.ml | 8 | ||||
| -rw-r--r-- | library/global.mli | 1 | ||||
| -rw-r--r-- | library/impargs.ml | 14 |
3 files changed, 10 insertions, 13 deletions
diff --git a/library/global.ml b/library/global.ml index 3f009d6d2..bbb77c853 100644 --- a/library/global.ml +++ b/library/global.ml @@ -68,4 +68,12 @@ let import cenv = global_env := import cenv !global_env let env_of_context hyps = reset_with_named_context hyps (env()) +open Nametab +let type_of_reference env = function + | VarRef id -> let (_,_,t) = Environ.lookup_named id env in t + | ConstRef c -> Environ.constant_type env c + | IndRef ind -> Inductive.type_of_inductive env ind + | ConstructRef cstr -> Inductive.type_of_constructor env cstr + +let type_of_global t = type_of_reference (env ()) t diff --git a/library/global.mli b/library/global.mli index 0a5edc9ad..6e352e2f8 100644 --- a/library/global.mli +++ b/library/global.mli @@ -52,4 +52,5 @@ val import : Environ.compiled_env -> unit (*s Function to get an environment from the constants part of the global environment and a given context. *) +val type_of_global : Nametab.global_reference -> types val env_of_context : Sign.named_context -> Environ.env diff --git a/library/impargs.ml b/library/impargs.ml index d6a7859a9..86acf1687 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -274,23 +274,11 @@ let context_of_global_reference = function | IndRef (sp,_) -> (Global.lookup_mind sp).mind_hyps | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps -let type_of_global r = - match r with - | VarRef id -> - let (_,_,ty) = lookup_named id (Global.env ()) in - ty - | ConstRef sp -> - Environ.constant_type (Global.env ()) sp - | IndRef sp -> - Inductive.type_of_inductive (Global.env ()) sp - | ConstructRef sp -> - Inductive.type_of_constructor (Global.env ()) sp - let check_range n i = if i<1 or i>n then error ("Bad argument number: "^(string_of_int i)) let declare_manual_implicits r l = - let t = type_of_global r in + let t = Global.type_of_global r in let n = List.length (fst (dest_prod (Global.env()) t)) in if not (list_distinct l) then error ("Some numbers occur several time"); List.iter (check_range n) l; |