diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-18 08:01:53 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-18 08:01:53 +0000 |
| commit | beac140c3970826bdfa104642301b9cee7530a97 (patch) | |
| tree | 7e6b854c99179e59351a80e012024d2ab0ef4dcc /kernel/reduction.mli | |
| parent | 37127f2d1e7be1abe8a07a93569507256fce1b1e (diff) | |
Restructuration des outils pour les inductifs.
- Les déclarations (mutual_inductive_packet et mutual_inductive_body),
utilisisées dans Environ vont dans Constant
- Instantiations du context local (mind_specif), instantiation des
paramètres globaux (inductive_family) et instantiation complète
(inductive_type, nouveau nom de inductive_summary) vont dans
Inductive qui est déplacé après réduction
- Certaines fonctions de Typeops et celle traitant des inductifs dans Reduction
sont regroupées dans Inductive
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@438 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 41 |
1 files changed, 7 insertions, 34 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index c772ede66..a1c542199 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -81,18 +81,13 @@ val whd_evar : 'a reduction_function val beta_applist : (constr * constr list) -> constr -val hnf_prod_app : - env -> 'a evar_map -> string -> constr -> constr -> constr -val hnf_prod_appvect : - env -> 'a evar_map -> string -> constr -> constr array -> constr -val hnf_prod_applist : - env -> 'a evar_map -> string -> constr -> constr list -> constr -val hnf_lam_app : - env -> 'a evar_map -> string -> constr -> constr -> constr -val hnf_lam_appvect : - env -> 'a evar_map -> string -> constr -> constr array -> constr -val hnf_lam_applist : - env -> 'a evar_map -> string -> constr -> constr list -> constr +val hnf_prod_app : env -> 'a evar_map -> constr -> constr -> constr +val hnf_prod_appvect : env -> 'a evar_map -> constr -> constr array -> constr +val hnf_prod_applist : env -> 'a evar_map -> constr -> constr list -> constr +val hnf_lam_app : env -> 'a evar_map -> constr -> constr -> constr +val hnf_lam_appvect : env -> 'a evar_map -> constr -> constr array -> constr +val hnf_lam_applist : env -> 'a evar_map -> constr -> constr list -> constr + val splay_prod : env -> 'a evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> 'a evar_map -> constr -> (name * constr) list * sorts val sort_of_arity : env -> constr -> sorts @@ -201,25 +196,3 @@ val whd_ise1_metas : 'a evar_map -> constr -> constr val hnf : env -> 'a evar_map -> constr -> constr * constr list val apprec : 'a stack_reduction_function val red_product : 'a reduction_function - -(* [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 - -(* [find_inductive env sigma t] raises [Induc] if [t] is not an inductive type*) -(* The resulting summary is relative to the current env *) -open Inductive -val find_inductive : env -> 'a evar_map -> constr -> inductive_summary - -val get_constructors : env -> 'a evar_map -> inductive_summary - -> constructor_summary array -val get_arity : env -> 'a evar_map -> inductive_summary -> - (name * constr) list * sorts - |