From 8c9ab46b0039b1944fbe008aa2bf98fcc5d0ae39 Mon Sep 17 00:00:00 2001
From: xclerc <xclerc@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 24 Oct 2013 14:06:07 +0000
Subject: Get rid of polymorphic equality in "checker/subtyping.ml".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16926 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/subtyping.ml | 25 +++++++++++++++----------
 1 file changed, 15 insertions(+), 10 deletions(-)

(limited to 'checker/subtyping.ml')

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 7903c33c5..070ed1924 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -129,14 +129,16 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   in
 
   let check_packet p1 p2 =
-    let check f = if f p1 <> f p2 then error () in
-      check (fun p -> p.mind_consnames);
-      check (fun p -> p.mind_typename);
+    let check eq f = if not (eq (f p1) (f p2)) then error () in
+    check
+      (fun a1 a2 -> Array.equal Id.equal a1 a2)
+      (fun p -> p.mind_consnames);
+      check Id.equal (fun p -> p.mind_typename);
       (* nf_lc later *)
       (* nf_arity later *)
       (* user_lc ignored *)
       (* user_arity ignored *)
-      check (fun p -> p.mind_nrealargs);
+      check Int.equal (fun p -> p.mind_nrealargs);
       (* kelim ignored *)
       (* listrec ignored *)
       (* finite done *)
@@ -151,9 +153,10 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       (arities_of_specif kn (mib1,p1))
       (arities_of_specif kn (mib2,p2))
   in
-  let check f = if f mib1 <> f mib2 then error () in
-  check (fun mib -> mib.mind_finite);
-  check (fun mib -> mib.mind_ntypes);
+  let check eq f = if not (eq (f mib1) (f mib2)) then error () in
+  let bool_equal (x : bool) (y : bool) = x = y in
+  check bool_equal (fun mib -> mib.mind_finite);
+  check Int.equal (fun mib -> mib.mind_ntypes);
   assert (Array.length mib1.mind_packets >= 1
 	    && Array.length mib2.mind_packets >= 1);
 
@@ -162,7 +165,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   (* at the time of checking the inductive arities in check_packet. *)
   (* Notice that we don't expect the local definitions to match: only *)
   (* the inductive types and constructors types have to be convertible *)
-  check (fun mib -> mib.mind_nparams);
+  check Int.equal (fun mib -> mib.mind_nparams);
 
   (*begin
     match mib2.mind_equiv with
@@ -176,7 +179,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
 	    if kn1 <> kn2 then error ()
   end;*)
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record);
+  check bool_equal (fun mib -> mib.mind_record);
   if mib1.mind_record then begin
     let rec names_prod_letin t = match t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
@@ -188,7 +191,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     assert (Array.length mib2.mind_packets = 1);
     assert (Array.length mib1.mind_packets.(0).mind_user_lc = 1);
     assert (Array.length mib2.mind_packets.(0).mind_user_lc = 1);
-    check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
+    check
+      (fun l1 l2 -> List.equal Name.equal l1 l2)
+      (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0));
   end;
   (* we first check simple things *)
   Array.iter2 check_packet mib1.mind_packets mib2.mind_packets;
-- 
cgit v1.2.3