aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/subtyping.ml25
1 files changed, 15 insertions, 10 deletions
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;