diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/sign.ml | 5 | ||||
| -rw-r--r-- | kernel/sign.mli | 3 |
2 files changed, 7 insertions, 1 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index aebb420f41..a90b43335a 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -71,7 +71,7 @@ let rel_context_nhyps hyps = let fold_rel_context f l ~init:x = List.fold_right f l x let fold_rel_context_reverse f ~init:x l = List.fold_left f x l -let map_rel_context f l = +let map_context f l = let map_decl (n, body_o, typ as decl) = let body_o' = option_smartmap f body_o in let typ' = f typ in @@ -80,6 +80,9 @@ let map_rel_context f l = in list_smartmap map_decl l +let map_rel_context = map_context +let map_named_context = map_context + (* Push named declarations on top of a rel context *) (* Bizarre. Should be avoided. *) let push_named_to_rel_context hyps ctxt = diff --git a/kernel/sign.mli b/kernel/sign.mli index 2bb921fe1e..052acfdc53 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -62,6 +62,9 @@ val fold_rel_context_reverse : (*s Map function of [rel_context] *) val map_rel_context : (constr -> constr) -> rel_context -> rel_context +(*s Map function of [named_context] *) +val map_named_context : (constr -> constr) -> named_context -> named_context + (*s Term constructors *) val it_mkLambda_or_LetIn : constr -> rel_context -> constr |