diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 20:49:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-18 20:49:43 +0000 |
| commit | a6369719fd0b81d3868afcbd18347e3d6ddfce65 (patch) | |
| tree | 0acb429c324f430e2138b59b0666e8a0625dbd1e /kernel | |
| parent | 9349f07465f69f2f9074f1b88515eef55c98fa6a (diff) | |
Added map_named_context
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6737 85f007b7-540e-0410-9357-904b9bb8a0f7
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 aebb420f4..a90b43335 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 2bb921fe1..052acfdc5 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 |