diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:52:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-28 18:58:06 +0100 |
| commit | 7b724139a09c5d875131c5861a32d225d5b4b07b (patch) | |
| tree | 3f556cc57d2b9500ecd972f97b2a25824c491dbe /kernel/declarations.ml | |
| parent | 8b42c73a6a3b417e848952e7510e27d74e6e1758 (diff) | |
Constructor type information uses the expanded form.
It used to simply remember the normal form of the type of the constructor.
This is somewhat problematic as this is ambiguous in presence of
let-bindings. Rather, we store this data in a fully expanded way, relying
on rel_contexts.
Probably fixes a crapload of bugs with inductive types containing
let-bindings, but it seems that not many were reported in the bugtracker.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 6777e0c223..567850645e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -166,7 +166,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 exposes the inductive type *) + mind_nf_lc : (rel_context * 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) *) |