From 05cf3fca1d0800e4cefaed3cb1825a8420ce9f2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 23 May 2020 20:41:23 +0200
Subject: Adding heterogeneous map on named contexts.

---
 kernel/context.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/context.mli')

diff --git a/kernel/context.mli b/kernel/context.mli
index 76c4461760..29309daf34 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -231,6 +231,9 @@ sig
     (** Map all terms in a given declaration. *)
     val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt
 
+    (** Map all terms, with an heterogeneous function. *)
+    val map_constr_het : ('a -> 'b) -> ('a, 'a) pt -> ('b, 'b) pt
+
     (** Perform a given action on all terms in a given declaration. *)
     val iter_constr : ('c -> unit) -> ('c, 'c) pt -> unit
 
-- 
cgit v1.2.3