diff options
Diffstat (limited to 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index a9a037bce..0144580bc 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -198,7 +198,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let record_equal x y = match x, y with | None, None -> true - | Some (p1,pb1), Some (p2,pb2) -> + | Some None, Some None -> true + | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) -> + Id.equal id1 id2 && Array.for_all2 eq_con_chk p1 p2 && Array.for_all2 eq_projection_body pb1 pb2 | _, _ -> false |