diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-16 10:58:13 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-12-17 17:47:48 +0100 |
| commit | fba1f0ed91aff372234b5a95422ee18f1730522f (patch) | |
| tree | fa5ca22e0af3ad47067c5908385039e1668f7843 /checker/subtyping.ml | |
| parent | f3a6d9080842899e50a44e9474ac0f9a475d5db1 (diff) | |
Update checker/values and cic due to changes in case_info and record_body.
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 |