diff options
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 2f33c60f5..1313208a3 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -264,14 +264,14 @@ type one_inductive_body = { mind_nf_lc : constr array; (** Head normalized constructor types so that their conclusion is atomic *) - mind_consnrealdecls : int array; - (** Length of the signature of the constructors (with let, w/o params) - (not used in the kernel) *) - mind_consnrealargs : int array; (** Length of the signature of the constructors (w/o let, w/o params) (not used in the kernel) *) + mind_consnrealdecls : int array; + (** Length of the signature of the constructors (with let, w/o params) + (not used in the kernel) *) + mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) (** {8 Datas for bytecode compilation } *) |