diff options
Diffstat (limited to 'lib/Conversion.ml')
| -rw-r--r-- | lib/Conversion.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/lib/Conversion.ml b/lib/Conversion.ml index b70a070..00bc942 100644 --- a/lib/Conversion.ml +++ b/lib/Conversion.ml @@ -18,11 +18,11 @@ struct let rec equate v1 v2 = match v1, v2 with | D.Neutral ne, v | v, D.Neutral ne -> equate_ne ne v - | D.Pi (base1, fam1), D.Pi (base2, fam2) -> + | D.Pi (_, base1, fam1), D.Pi (_, base2, fam2) -> equate base1 base2; equate_clo fam1 fam2 - | D.Lam clo1, D.Lam clo2 -> equate_clo clo1 clo2 - | D.Sg (base1, fam1), D.Sg (base2, fam2) -> + | D.Lam (_, clo1), D.Lam (_, clo2) -> equate_clo clo1 clo2 + | D.Sg (_, base1, fam1), D.Sg (_, base2, fam2) -> equate base1 base2; equate_clo fam1 fam2 | D.Pair (fst1, snd1), D.Pair (fst2, snd2) -> @@ -44,8 +44,8 @@ struct | D.App arg1, D.App arg2 -> equate arg1 arg2 | D.Fst, D.Fst -> () | D.Snd, D.Snd -> () - | D.BoolElim { cmot = mot1; vtrue = t1; vfalse = f1 }, - D.BoolElim { cmot = mot2; vtrue = t2; vfalse = f2 } -> + | D.BoolElim { motive = mot1; true_case = t1; false_case = f1; _ }, + D.BoolElim { motive = mot2; true_case = t2; false_case = f2; _ } -> equate_clo mot1 mot2; equate t1 t2; equate f1 f2; @@ -63,7 +63,7 @@ struct equate_ne_head hd hd2; equate_spine sp sp2 (* eta expansion *) - | D.Lam clo -> bind @@ fun arg -> + | D.Lam (_, clo) -> bind @@ fun arg -> equate_ne (hd, sp <: D.App arg) (Eval.inst_clo clo arg) | D.Pair (fst, snd) -> equate_ne (hd, sp <: D.Fst) fst; |