diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-14 14:30:06 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-01-14 14:30:06 +0000 |
| commit | b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 (patch) | |
| tree | 329838825dc03d431fc36489fdc818ca04d4bd2a /library/global.ml | |
| parent | 6dbc9f181b90216958fd9d87f8426901b1e4c37e (diff) | |
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body)
instead of looking it up in the environment. A version of the same functions
with the old type is put in Inductiveops (outside the kernel).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/global.ml')
| -rw-r--r-- | library/global.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/library/global.ml b/library/global.ml index 9ad01842c..660620086 100644 --- a/library/global.ml +++ b/library/global.ml @@ -134,7 +134,12 @@ open Libnames 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 + | 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 |