diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1e2cedee29..289968eb53 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -78,8 +78,6 @@ let instantiate_params full t args sign = if rem_args <> [] then fail(); substl subs ty -let instantiate_partial_params = instantiate_params false - let full_inductive_instantiate mib params sign = let dummy = prop_sort in let t = mkArity (sign,dummy) in @@ -95,10 +93,6 @@ let full_constructor_instantiate ((mind,_),(mib,_),params) = (* Functions to build standard types related to inductive *) - -let number_of_inductives mib = Array.length mib.mind_packets -let number_of_constructors mip = Array.length mip.mind_consnames - (* Computing the actual sort of an applied or partially applied inductive type: |