diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-25 17:47:43 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-25 17:48:30 +0100 |
| commit | 89978bc0c60a4d9d616d18cb36014ac4cce8c48f (patch) | |
| tree | 987b2fdd9c089c6f3827ff3d7f0b9dc8cbb4d95f /checker/declarations.ml | |
| parent | 765c6b15b76fd407a4d888d3f5e8cc532901045b (diff) | |
[checker] Avoid relying on canonical names.
Fixes #5747: "make validate" fails with "bad recursive trees"
Diffstat (limited to 'checker/declarations.ml')
| -rw-r--r-- | checker/declarations.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/checker/declarations.ml b/checker/declarations.ml index 884a1ef18..15b1f0a0c 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -484,8 +484,8 @@ let subst_wf_paths sub p = Rtree.smartmap (subst_recarg sub) p let eq_recarg r1 r2 = match r1, r2 with | Norec, Norec -> true - | Mrec i1, Mrec i2 -> Names.eq_ind i1 i2 - | Imbr i1, Imbr i2 -> Names.eq_ind i1 i2 + | Mrec i1, Mrec i2 -> Names.eq_ind_chk i1 i2 + | Imbr i1, Imbr i2 -> Names.eq_ind_chk i1 i2 | _ -> false let eq_wf_paths = Rtree.equal eq_recarg |