diff options
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index d81904cc..b9d0f984 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductive.mli 8871 2006-05-28 16:46:48Z herbelin $ i*) +(*i $Id: inductive.mli 9314 2006-10-29 20:11:08Z herbelin $ i*) (*i*) open Names @@ -35,8 +35,9 @@ type mind_specif = mutual_inductive_body * one_inductive_body val lookup_mind_specif : env -> inductive -> mind_specif (*s Functions to build standard types related to inductive *) +val ind_subst : mutual_inductive -> mutual_inductive_body -> constr list -val type_of_inductive : mind_specif -> types +val type_of_inductive : env -> mind_specif -> types val elim_sorts : mind_specif -> sorts_family list @@ -49,6 +50,7 @@ val arities_of_constructors : inductive -> mind_specif -> types array (* Transforms inductive specification into types (in nf) *) val arities_of_specif : mutual_inductive -> mind_specif -> types array + (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: <p>Cases (c :: (I args)) of b1..bn end @@ -78,10 +80,11 @@ val check_cofix : env -> cofixpoint -> unit val type_of_inductive_knowing_parameters : env -> one_inductive_body -> types array -> types -val set_inductive_level : env -> sorts -> types -> types - val max_inductive_sort : sorts array -> universe +val instantiate_universes : env -> Sign.rel_context -> + polymorphic_arity -> types array -> Sign.rel_context * sorts + (***************************************************************) (* Debug *) |