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 --- pretyping/inductiveops.mli | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'pretyping/inductiveops.mli') 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 : -- cgit v1.2.3