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.ml | 9 +++++++++
 1 file changed, 9 insertions(+)

(limited to 'kernel/context.ml')

diff --git a/kernel/context.ml b/kernel/context.ml
index 6a99f201f3..ab66898b59 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -365,6 +365,15 @@ struct
           let ty' = f ty in
           if v == v' && ty == ty' then decl else LocalDef (id, v', ty')
 
+    let map_constr_het f = function
+      | LocalAssum (id, ty) ->
+          let ty' = f ty in
+          LocalAssum (id, ty')
+      | LocalDef (id, v, ty) ->
+          let v' = f v in
+          let ty' = f ty in
+          LocalDef (id, v', ty')
+
     (** Perform a given action on all terms in a given declaration. *)
     let iter_constr f = function
       | LocalAssum (_, ty) -> f ty
-- 
cgit v1.2.3