From c1729637d4fe32ebe0268eb338fcf4d032bb5df7 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Mar 2015 11:26:21 +0100
Subject: Fully fixing bug #3491 (anomaly when building _rect scheme in the
 presence of let-ins and recursively non-uniform parameters).

The bug was in the List.chop of Inductiveops.get_arity which was wrong
in the presence of let-ins and recursively non-uniform parameters.

The bug #3491 showed up because, in addition to have let-ins, it was
wrongly detected as having recursively non-uniform parameters.

Also added some comments in declarations.mli.
---
 kernel/declarations.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index cef920c6a5..c68e39ce33 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -139,7 +139,7 @@ type one_inductive_body = {
 
     mind_kelim : sorts_family list; (** List of allowed elimination sorts *)
 
-    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *)
+    mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion exposes the inductive type *)
 
     mind_consnrealargs : int array;
  (** Number of expected proper arguments of the constructors (w/o params)
@@ -172,7 +172,7 @@ type mutual_inductive_body = {
 
     mind_hyps : Context.section_context;  (** Section hypotheses on which the block depends *)
 
-    mind_nparams : int;  (** Number of expected parameters *)
+    mind_nparams : int;  (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *)
 
     mind_nparams_rec : int;  (** Number of recursively uniform (i.e. ordinary) parameters *)
 
-- 
cgit v1.2.3