From 89978bc0c60a4d9d616d18cb36014ac4cce8c48f Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
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 ++--
 checker/inductive.ml    | 10 +++++-----
 2 files changed, 7 insertions(+), 7 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
diff --git a/checker/inductive.ml b/checker/inductive.ml
index fb33cd96b..8d426a3c0 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -381,7 +381,7 @@ let type_case_branches env (pind,largs) (p,pj) c =
 let check_case_info env indsp ci =
   let (mib,mip) = lookup_mind_specif env indsp in
   if
-    not (eq_ind indsp ci.ci_ind) ||
+    not (eq_ind_chk indsp ci.ci_ind) ||
     (mib.mind_nparams <> ci.ci_npar) ||
     (mip.mind_consnrealdecls <> ci.ci_cstr_ndecls) ||
     (mip.mind_consnrealargs <> ci.ci_cstr_nargs)
@@ -441,8 +441,8 @@ let inter_recarg r1 r2 = match r1, r2 with
 | Norec, Norec -> Some r1
 | Mrec i1, Mrec i2
 | Imbr i1, Imbr i2
-| Mrec i1, Imbr i2 -> if Names.eq_ind i1 i2 then Some r1 else None
-| Imbr i1, Mrec i2 -> if Names.eq_ind i1 i2 then Some r2 else None
+| Mrec i1, Imbr i2 -> if Names.eq_ind_chk i1 i2 then Some r1 else None
+| Imbr i1, Mrec i2 -> if Names.eq_ind_chk i1 i2 then Some r2 else None
 | _ -> None
 
 let inter_wf_paths = Rtree.inter eq_recarg inter_recarg Norec
@@ -538,7 +538,7 @@ let lookup_subterms env ind =
 
 let match_inductive ind ra =
   match ra with
-    | (Mrec i | Imbr i) -> eq_ind ind i
+    | (Mrec i | Imbr i) -> eq_ind_chk ind i
     | Norec -> false
 
 (* In {match c as z in ci y_s return P with |C_i x_s => t end}
@@ -639,7 +639,7 @@ let get_recargs_approx env tree ind args =
        (* When the inferred tree allows it, we consider that we have a potential
        nested inductive type *)
        begin match dest_recarg tree with
-	     | Imbr kn' | Mrec kn' when eq_ind (fst ind_kn) kn' ->
+             | Imbr kn' | Mrec kn' when eq_ind_chk (fst ind_kn) kn' ->
 			   build_recargs_nested ienv tree (ind_kn, largs)
 	     | _ -> mk_norec
        end
-- 
cgit v1.2.3