From 001ff72b2c17fb7b2fcaefa2555c115f0d909a03 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Mon, 28 Oct 2013 14:08:46 +0100
Subject: Initial work on reintroducing old-style polymorphism for
 compatibility (the stdlib does not compile entirely).

---
 kernel/declareops.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/declareops.mli')

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
-- 
cgit v1.2.3