From 89978bc0c60a4d9d616d18cb36014ac4cce8c48f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 25 Jan 2018 17:47:43 +0100 Subject: [checker] Avoid relying on canonical names. Fixes #5747: "make validate" fails with "bad recursive trees" --- checker/declarations.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'checker/declarations.ml') 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 -- cgit v1.2.3