diff options
| author | herbelin | 2000-05-31 11:43:21 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-31 11:43:21 +0000 |
| commit | a6974254f3c46683d93ced625430d0fef26bebe5 (patch) | |
| tree | 48a2f915d6766a81c0ee74cd073fb45eb49ad373 /kernel/inductive.mli | |
| parent | a87fc0236aa3dd9135ff75a890ba8f5c0a05a419 (diff) | |
Nettoyage de Generic;Suppression des DLAM en tête des listes de constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@480 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b603fbf1ee..fa989110cb 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -43,8 +43,7 @@ val mis_consnames : inductive_instance -> identifier array val mis_typed_arity : inductive_instance -> typed_type val mis_inductive : inductive_instance -> inductive val mis_arity : inductive_instance -> constr -val mis_lc : inductive_instance -> constr -val mis_lc_without_abstractions : inductive_instance -> constr array +val mis_lc : inductive_instance -> constr array val mis_type_mconstructs : inductive_instance -> constr array * constr array val mis_type_mconstruct : int -> inductive_instance -> constr val mis_params_ctxt : inductive_instance -> (name * constr) list @@ -58,8 +57,8 @@ val dest_ind_family : inductive_family -> inductive_instance * constr list val liftn_inductive_family : int -> int -> inductive_family -> inductive_family val lift_inductive_family : int -> inductive_family -> inductive_family -val substn_many_ind_family : constr Generic.substituend array -> int - -> inductive_family -> inductive_family +val substnl_ind_family : constr list -> int -> inductive_family + -> inductive_family (*s [inductive_type] = [inductive_family] applied to ``real'' parameters *) type inductive_type = IndType of inductive_family * constr list @@ -71,8 +70,7 @@ val mkAppliedInd : inductive_type -> constr val liftn_inductive_type : int -> int -> inductive_type -> inductive_type val lift_inductive_type : int -> inductive_type -> inductive_type -val substn_many_ind_type : constr Generic.substituend array -> int - -> inductive_type -> inductive_type +val substnl_ind_type : constr list -> int -> inductive_type -> inductive_type (*s A [constructor] is an [inductive] + an index; the following functions destructs and builds [constructor] *) |