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/inductive.mli | |
| 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/inductive.mli')
| -rw-r--r-- | kernel/inductive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 3c1464c6c9..ad35c16c22 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -139,4 +139,4 @@ val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec val lambda_implicit_lift : int -> constr -> constr -val abstract_mind_lc : int -> Int.t -> constr array -> constr array +val abstract_mind_lc : int -> Int.t -> (rel_context * constr) array -> constr array |