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

3 files changed, 24 insertions, 8 deletions

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 *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ee92d8f2a5..52af27747e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -73,11 +73,11 @@ val allowed_sorts : env -> inductive -> sorts_family list
 (** Extract information from an inductive family *)
 
 type constructor_summary = {
-  cs_cstr : constructor;
-  cs_params : constr list;
-  cs_nargs : int;
-  cs_args : rel_context;
-  cs_concl_realargs : constr array;
+  cs_cstr : constructor;    (* internal name of the constructor *)
+  cs_params : constr list;  (* parameters of the constructor in current ctx *)
+  cs_nargs : int;           (* length of arguments signature (letin included) *)
+  cs_args : rel_context;    (* signature of the arguments (letin included) *)
+  cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
 }
 val lift_constructor : int -> constructor_summary -> constructor_summary
 val get_constructor :