diff options
| author | Pierre-Marie Pédrot | 2020-09-23 12:42:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-21 12:22:12 +0200 |
| commit | bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc (patch) | |
| tree | 6cf8e0f459ff3630ebd5115773c04bc0bcd70b6c /kernel/nativeconv.ml | |
| parent | 0a46af10ffc38726207bca952775102d48ad3b15 (diff) | |
Introduce an Ind module in the Names API.
This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 00418009c7..76215b4386 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -80,7 +80,7 @@ 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.CanOrd.equal c1 c2 then convert_instances ~flex:true u1 u2 cu @@ -90,7 +90,7 @@ and conv_atom env pb lvl a1 a2 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 _, _ |