diff options
Diffstat (limited to 'kernel/instantiate.mli')
| -rw-r--r-- | kernel/instantiate.mli | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index 8d267021f5..302927074e 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -28,12 +28,3 @@ val existential_value : 'a evar_map -> constr -> constr val existential_type : 'a evar_map -> constr -> constr val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option - -val mis_typed_arity : mind_specif -> typed_type -val mis_arity : mind_specif -> constr - -val mis_lc : mind_specif -> constr -val mis_lc_without_abstractions : mind_specif -> constr array - -val mis_type_mconstructs : mind_specif -> constr array * constr array - |