From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 pretyping/miscops.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'pretyping/miscops.ml')

diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 142e430ff8..7fe81c9a43 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -58,3 +58,16 @@ let map_red_expr_gen f g h = function
   | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
   | Cbn flags -> Cbn (map_flags g flags)
   | ExtraRedExpr _ | Red _ | Hnf as x -> x
+
+(** Mapping bindings *)
+
+let map_explicit_bindings f l =
+  let map (loc, hyp, x) = (loc, hyp, f x) in
+  List.map map l
+
+let map_bindings f = function
+| ImplicitBindings l -> ImplicitBindings (List.map f l)
+| ExplicitBindings expl -> ExplicitBindings (map_explicit_bindings f expl)
+| NoBindings -> NoBindings
+
+let map_with_bindings f (x, bl) = (f x, map_bindings f bl)
-- 
cgit v1.2.3