diff options
Diffstat (limited to 'pretyping/inductiveops.mli')
| -rw-r--r-- | pretyping/inductiveops.mli | 10 |
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 : |