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 /checker/checkInductive.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 'checker/checkInductive.ml')
| -rw-r--r-- | checker/checkInductive.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml index 4329b2d743..b681fb876e 100644 --- a/checker/checkInductive.ml +++ b/checker/checkInductive.ml @@ -89,6 +89,9 @@ let eq_recarg a1 a2 = match a1, a2 with let eq_reloc_tbl = Array.equal (fun x y -> Int.equal (fst x) (fst y) && Int.equal (snd x) (snd y)) +let eq_in_context (ctx1, t1) (ctx2, t2) = + Context.Rel.equal Constr.equal ctx1 ctx2 && Constr.equal t1 t2 + let check_packet env mind ind { mind_typename; mind_arity_ctxt; mind_arity; mind_consnames; mind_user_lc; mind_nrealargs; mind_nrealdecls; mind_kelim; mind_nf_lc; @@ -105,7 +108,7 @@ let check_packet env mind ind check "mind_nrealdecls" Int.(equal ind.mind_nrealdecls mind_nrealdecls); check "mind_kelim" (check_kelim ind.mind_kelim mind_kelim); - check "mind_nf_lc" (Array.equal Constr.equal ind.mind_nf_lc mind_nf_lc); + check "mind_nf_lc" (Array.equal eq_in_context ind.mind_nf_lc mind_nf_lc); (* NB: here syntactic equality is not just an optimisation, we also care about the shape of the terms *) |