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/typeops.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/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 22 |
1 files changed, 5 insertions, 17 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2c93141cb..7ab2404f8 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -41,7 +41,7 @@ val type_of_case : env -> 'a evar_map -> case_info -> unsafe_judgment array -> unsafe_judgment val type_case_branches : - env -> 'a evar_map -> Inductive.inductive_summary -> constr -> constr + env -> 'a evar_map -> Inductive.inductive_type -> constr -> constr -> constr -> constr array * constr val judge_of_prop_contents : contents -> unsafe_judgment @@ -74,25 +74,13 @@ val control_only_guard : env -> 'a evar_map -> constr -> unit val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array -> unsafe_judgment array -> constraints -val type_one_branch_dep : env -> 'a evar_map -> - int * constr list * constr -> constr -> constr -> constr - -val type_one_branch_nodep : env -> 'a evar_map -> - int * constr list * constr -> constr -> constr - -val make_arity_dep : - env -> 'a evar_map -> constr -> constr -> constr -> constr - -val make_arity_nodep : - env -> 'a evar_map -> constr -> constr -> constr +open Inductive val find_case_dep_nparams : - env -> 'a evar_map -> constr * constr -> - inductive * constr list -> constr -> bool + env -> 'a evar_map -> constr * constr -> inductive_family -> constr -> bool -(* The constr list is the global args list *) -val type_inst_construct : - env -> 'a evar_map -> int -> inductive * constr list -> constr +(* Returns the type of the [i]$^{th}$ constructor of the inductive family *) +val type_inst_construct : int -> inductive_family -> constr val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool |