diff options
| author | sacerdot | 2005-01-14 14:30:06 +0000 |
|---|---|---|
| committer | sacerdot | 2005-01-14 14:30:06 +0000 |
| commit | b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 (patch) | |
| tree | 329838825dc03d431fc36489fdc818ca04d4bd2a /kernel/inductive.mli | |
| 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 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 0ecfe2a8c4..0174b80201 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -28,24 +28,24 @@ val find_rectype : env -> types -> inductive * constr list val find_inductive : env -> types -> inductive * constr list val find_coinductive : env -> types -> inductive * constr list +type mind_specif = mutual_inductive_body * one_inductive_body + (*s Fetching information in the environment about an inductive type. Raises [Not_found] if the inductive type is not found. *) -val lookup_mind_specif : - env -> inductive -> mutual_inductive_body * one_inductive_body +val lookup_mind_specif : env -> inductive -> mind_specif (*s Functions to build standard types related to inductive *) -val type_of_inductive : env -> inductive -> types +val type_of_inductive : mind_specif -> types (* Return type as quoted by the user *) -val type_of_constructor : env -> constructor -> types +val type_of_constructor : constructor -> mind_specif -> types (* Return constructor types in normal form *) -val arities_of_constructors : env -> inductive -> types array +val arities_of_constructors : inductive -> mind_specif -> types array (* Transforms inductive specification into types (in nf) *) -val arities_of_specif : mutual_inductive -> - mutual_inductive_body * one_inductive_body -> types array +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: |