diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-28 14:08:46 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:54 +0200 |
| commit | 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 (patch) | |
| tree | 9e83ae395173699a7c5b6f00648c4336bedb7afd /kernel/declareops.mli | |
| parent | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (diff) | |
Initial work on reintroducing old-style polymorphism for compatibility (the stdlib does not compile entirely).
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 |