From 9600a6960debedbe1bc941aff383fab37a546b94 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 6 Apr 2011 17:00:38 +0000
Subject: A few extra combinators about rel_declaration/named_declaration + a
 bit of doc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13959 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.ml  | 12 +++++++++---
 kernel/term.mli | 10 ++++++++++
 2 files changed, 19 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/term.ml b/kernel/term.ml
index 8fcbec7abd..453cc4c179 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -814,6 +814,12 @@ let map_rel_declaration = map_named_declaration
 let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a)
 let fold_rel_declaration = fold_named_declaration
 
+let exists_named_declaration f (_, v, ty) = Option.cata f false v || f ty
+let exists_rel_declaration f (_, v, ty) = Option.cata f false v || f ty
+
+let for_all_named_declaration f (_, v, ty) = Option.cata f true v && f ty
+let for_all_rel_declaration f (_, v, ty) = Option.cata f true v && f ty
+
 (***************************************************************************)
 (*     Type of local contexts (telescopes)                                 *)
 (***************************************************************************)
@@ -969,12 +975,12 @@ let substnl laml n =
 let substl laml = substnl laml 0
 let subst1 lam = substl [lam]
 
-let substnl_decl laml k (id,bodyopt,typ) =
-  (id,Option.map (substnl laml k) bodyopt,substnl laml k typ)
+let substnl_decl laml k = map_rel_declaration (substnl laml k)
 let substl_decl laml = substnl_decl laml 0
 let subst1_decl lam = substl_decl [lam]
-let subst1_named_decl = subst1_decl
+let substnl_named laml k = map_named_declaration (substnl laml k)
 let substl_named_decl = substl_decl
+let subst1_named_decl = subst1_decl
 
 (* (thin_val sigma) removes identity substitutions from sigma *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index f92471ce03..008cad9947 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -344,6 +344,16 @@ val fold_named_declaration :
 val fold_rel_declaration :
   (constr -> 'a -> 'a) -> rel_declaration -> 'a -> 'a
 
+val exists_named_declaration :
+  (constr -> bool) -> named_declaration -> bool
+val exists_rel_declaration :
+  (constr -> bool) -> rel_declaration -> bool
+
+val for_all_named_declaration :
+  (constr -> bool) -> named_declaration -> bool
+val for_all_rel_declaration :
+  (constr -> bool) -> rel_declaration -> bool
+
 (** {6 Contexts of declarations referred to by de Bruijn indices } *)
 
 (** In [rel_context], more recent declaration is on top *)
-- 
cgit v1.2.3