diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-11 21:55:33 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:28:47 +0100 |
| commit | 0489e8b56d7e10f7111c0171960e25d32201b963 (patch) | |
| tree | d0d71a6a239a7297faea5707bdc88edba6a98e83 /pretyping/miscops.ml | |
| parent | cbea91d815f134d63d02d8fb1bd78ed97db28cd1 (diff) | |
Clenv API using EConstr.
Diffstat (limited to 'pretyping/miscops.ml')
| -rw-r--r-- | pretyping/miscops.ml | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml index 142e430ff..7fe81c9a4 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) |