diff options
| author | herbelin | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e /kernel/reduction.mli | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
Nouveaux types 'constructor' et 'inductive' dans Term;
les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 28 |
1 files changed, 17 insertions, 11 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index dd06af8adc..6638f30ee0 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -14,7 +14,6 @@ open Closure (* Reduction Functions. *) exception Redelimination -exception Induc exception Elimconst type 'a reduction_function = env -> 'a evar_map -> constr -> constr @@ -191,18 +190,25 @@ val whd_ise1 : 'a evar_map -> constr -> constr val nf_ise1 : 'a evar_map -> constr -> constr val whd_ise1_metas : 'a evar_map -> constr -> constr - (*s Obsolete Reduction Functions *) val hnf : env -> 'a evar_map -> constr -> constr * constr list val apprec : 'a stack_reduction_function val red_product : 'a reduction_function -val find_mrectype : - env -> 'a evar_map -> constr -> constr * constr list -val find_minductype : - env -> 'a evar_map -> constr -> constr * constr list -val find_mcoinductype : - env -> 'a evar_map -> constr -> constr * constr list -val check_mrectype_spec : env -> 'a evar_map -> constr -> constr -val minductype_spec : env -> 'a evar_map -> constr -> constr -val mrectype_spec : env -> 'a evar_map -> constr -> constr + +(* [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 + +(* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*) +(* The resulting summary is relative to the current env *) +val try_mutind_of : env -> 'a evar_map -> constr -> Inductive.inductive_summary + + |