diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:21:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 17:21:17 +0000 |
commit | 08f5f4b1268624de1f8733ce30b51a62080f6ba6 (patch) | |
tree | a9cebdf444e0b1fdcd77e00d725a7905cafe6ff0 /kernel/inductive.mli | |
parent | abcf77362c7744ade443307d62dcb30e9025541a (diff) |
suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@464 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
-rw-r--r-- | kernel/inductive.mli | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b7501dd64..b603fbf1e 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -128,17 +128,24 @@ val make_arity : env -> 'a evar_map -> bool -> inductive_family -> val build_branch_type : env -> bool -> constr -> constructor_summary -> constr -(*s [find_m*type env sigma c] coerce [c] to an recursive type (I args). +(*s Extracting an inductive type from a constructions *) + +exception Induc + +(* [extract_mrectype c] assumes [c] is syntactically an inductive type + applied to arguments then it returns its components; if not an + inductive type, it raises [Induc] *) +val extract_mrectype : constr -> inductive * constr list + +(* [find_m*type env sigma c] coerce [c] to an recursive type (I args). [find_mrectype], [find_minductype] and [find_mcoinductype] respectively accepts any recursive type, only an inductive type and only a coinductive type. They raise [Induc] if not convertible to a recursive type. *) -exception Induc val find_mrectype : env -> 'a evar_map -> constr -> inductive * constr list val find_minductype : env -> 'a evar_map -> constr -> inductive * constr list val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list -val extract_mrectype : env -> 'a evar_map -> constr -> inductive * constr list val lookup_mind_specif : inductive -> env -> inductive_instance |