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

1 files changed, 5 insertions, 5 deletions

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index ee92d8f2a..52af27747 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 :