diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-06 11:27:09 +0200 |
| commit | 0413899668e8be15df5065abdaf1d40ad3c2c31b (patch) | |
| tree | 5d2c4671737b9d0c9eba68cdf0d16503c6e47608 /checker/cic.mli | |
| parent | d7db69dea59cddd3ac81ed469170fad889af4e16 (diff) | |
Fix checker to handle projections with eta and universe polymorphism correctly.
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 } *) |