diff options
Diffstat (limited to 'kernel/declareops.mli')
| -rw-r--r-- | kernel/declareops.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0c5f3584e..9f5197668 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -12,6 +12,11 @@ open Mod_subst (** Operations concerning types in [Declarations] : [constant_body], [mutual_inductive_body], [module_body] ... *) +(** {6 Arities} *) + +val map_decl_arity : ('a -> 'c) -> ('b -> 'd) -> + ('a, 'b) declaration_arity -> ('c, 'd) declaration_arity + (** {6 Constants} *) val subst_const_body : substitution -> constant_body -> constant_body |