diff options
| author | coqbot-app[bot] | 2020-10-27 12:55:13 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-27 12:55:13 +0000 |
| commit | 5f5cddae48c08872107f30938dcc2f3c8d91f33a (patch) | |
| tree | 2f1bb58c33fee5b4bb0913296ef4341a8832feb4 /kernel/nativeconv.ml | |
| parent | b87fd6cfe5fe872a38d98c294aea84cde8c6c160 (diff) | |
| parent | 375fc707b402b855770ec32c57ad1362f2a89e5c (diff) | |
Merge PR #13075: Introducing the foundations for a name-alias-agnostic API
Reviewed-by: SkySkimmer
Ack-by: gares
Ack-by: ejgallego
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index fc6afb79d4..76215b4386 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -80,17 +80,17 @@ and conv_atom env pb lvl a1 a2 cu = | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> - if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + if Ind.CanOrd.equal ind1 ind2 then convert_instances ~flex:false u1 u2 cu else raise NotConvertible | Aconstant (c1,u1), Aconstant (c2,u2) -> - if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 cu + if Constant.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu else raise NotConvertible | Asort s1, Asort s2 -> sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> if Id.equal id1 id2 then cu else raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> - if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; + if not (Ind.CanOrd.equal a1.asw_ind a2.asw_ind) then raise NotConvertible; let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in @@ -124,7 +124,7 @@ and conv_atom env pb lvl a1 a2 cu = let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> - if not (eq_ind ind1 ind2 && Int.equal i1 i2) then raise NotConvertible + if not (Ind.CanOrd.equal ind1 ind2 && Int.equal i1 i2) then raise NotConvertible else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ |