diff options
| author | coq | 2002-08-16 10:00:36 +0000 |
|---|---|---|
| committer | coq | 2002-08-16 10:00:36 +0000 |
| commit | b1eef69751a05eebdbdc9d3091e1dae3386218d0 (patch) | |
| tree | e7c3c7b3657f1d15e6931e71f77d1da4114d2b2c /kernel/inductive.mli | |
| parent | a1858ecd34bd7946dab7e7fbf2413036f78f7109 (diff) | |
Strengthenning rules for modules + No modules in sections
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index f279eb79aa..a6ce7d42e8 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -44,8 +44,8 @@ val type_of_constructor : env -> constructor -> types val arities_of_constructors : env -> inductive -> types array (* Transforms inductive specification into types (in nf) *) -val arities_of_specif : - kernel_name -> mutual_inductive_body * one_inductive_body -> types array +val arities_of_specif : mutual_inductive -> + mutual_inductive_body * one_inductive_body -> types array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: @@ -62,6 +62,10 @@ val type_case_branches : given inductive type. *) val check_case_info : env -> inductive -> case_info -> unit +(* Find the ultimate inductive in the mind_equiv chain *) + +val scrape_mind : env -> mutual_inductive -> mutual_inductive + (*s Guard conditions for fix and cofix-points. *) val check_fix : env -> fixpoint -> unit val check_cofix : env -> cofixpoint -> unit |