diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /pretyping/inductiveops.ml | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e0cdeeee..14136f61 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductiveops.ml 8845 2006-05-23 07:41:58Z herbelin $ *) +(* $Id: inductiveops.ml 9310 2006-10-28 19:35:09Z herbelin $ *) open Util open Names @@ -23,7 +23,7 @@ open Reductionops let type_of_inductive env ind = let specif = Inductive.lookup_mind_specif env ind in - Inductive.type_of_inductive specif + Inductive.type_of_inductive env specif (* Return type as quoted by the user *) let type_of_constructor env cstr = @@ -126,6 +126,10 @@ let inductive_nargs env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mib.mind_nparams, mip.mind_nrealargs +let allowed_sorts env (kn,i as ind) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_kelim + (* Annotation for cases *) let make_case_info env ind style pats_source = let (mib,mip) = Inductive.lookup_mind_specif env ind in |