From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 checker/subtyping.ml | 32 ++++++++++++--------------------
 1 file changed, 12 insertions(+), 20 deletions(-)

(limited to 'checker/subtyping.ml')

diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 31dab0c9..0916d98d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Cic
-open Term
 open Declarations
 open Environ
 open Reduction
@@ -123,16 +122,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
-  let eq_projection_body p1 p2 =
-    let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check MutInd.equal (fun x -> x.proj_ind);
-    check (==) (fun x -> x.proj_npars);
-    check (==) (fun x -> x.proj_arg);
-    check (eq_constr) (fun x -> x.proj_type);
-    check (eq_constr) (fun x -> fst x.proj_eta);
-    check (eq_constr) (fun x -> snd x.proj_eta);
-    check (eq_constr) (fun x -> x.proj_body); true
-  in
   let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
@@ -186,16 +175,19 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   (* we check that records and their field names are preserved. *)
   let record_equal x y =
     match x, y with
-    | None, None -> true
-    | Some None, Some None -> true
-    | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
-      Id.equal id1 id2 &&
-      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-      Array.for_all2 eq_projection_body pb1 pb2
+    | NotRecord, NotRecord -> true
+    | FakeRecord, FakeRecord -> true
+    | PrimRecord info1, PrimRecord info2 ->
+      let check (id1, p1, pb1) (id2, p2, pb2) =
+        (* we don't care about the id, the types are inferred from the inductive
+           (ie checked before now) *)
+        Array.for_all2 Label.equal p1 p2
+      in
+      Array.equal check info1 info2
     | _, _ -> false
   in
   check record_equal (fun mib -> mib.mind_record);
-  if mib1.mind_record != None then begin
+  if mib1.mind_record != NotRecord then begin
     let rec names_prod_letin t = match t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
@@ -216,7 +208,7 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets
   in ()
 
-let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
+let check_constant env l info1 cb2 spec2 subst1 subst2 =
   let error () = error_not_match l spec2 in
   let check_conv f = check_conv_error error f in
   let check_type env t1 t2 = check_conv conv_leq env t1 t2 in
@@ -280,7 +272,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
   let check_one_body  (l,spec2) =
       match spec2 with
 	| SFBconst cb2 ->
-	    check_constant  env mp1 l (get_obj mp1 map1 l)
+            check_constant env l (get_obj mp1 map1 l)
 	      cb2 spec2 subst1 subst2
 	| SFBmind mib2 ->
 	    check_inductive env mp1 l (get_obj mp1 map1 l)
-- 
cgit v1.2.3