diff options
| author | filliatr | 1999-08-30 13:17:26 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-30 13:17:26 +0000 |
| commit | f1874a538ef7e5886b72c2ec2ce21b23d05aa8d7 (patch) | |
| tree | d54f85de98bbc0a137a3edeed213918a46e26374 /kernel/indtypes.mli | |
| parent | 19d21ec59b69a7bd5a8e4e77794e85fed6b48d39 (diff) | |
ajout des inductifs (sans types singletons pour l'instant)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@32 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 8723ec3c65..ebb1e1f679 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -2,6 +2,8 @@ (* $Id$ *) (*i*) +open Names +open Term open Inductive open Environ (*i*) @@ -10,3 +12,11 @@ open Environ inductive types are some arities. *) val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit + +val sort_of_arity : 'a unsafe_env -> constr -> sorts + +val cci_inductive : + 'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> + (identifier * typed_type * identifier list * bool * bool * constr) list -> + mutual_inductive_body + |