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/reduction.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/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 96bf370342..5589ae3483 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -283,7 +283,7 @@ let convert_constructors ctor nargs u1 u2 (s, check) = let conv_table_key infos k1 k2 cuniv = if k1 == k2 then cuniv else match k1, k2 with - | ConstKey (cst, u), ConstKey (cst', u') when Constant.equal cst cst' -> + | ConstKey (cst, u), ConstKey (cst', u') when Constant.CanOrd.equal cst cst' -> if Univ.Instance.equal u u' then cuniv else let flex = evaluable_constant cst (info_env infos) @@ -441,7 +441,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = | Some s2 -> eqappr cv_pb l2r infos appr1 (lft2, (c2, (s2 :: v2))) cuniv | None -> - if Projection.Repr.equal (Projection.repr p1) (Projection.repr p2) + if Projection.Repr.CanOrd.equal (Projection.repr p1) (Projection.repr p2) && compare_stack_shape v1 v2 then let el1 = el_stack lft1 v1 in let el2 = el_stack lft2 v2 in @@ -568,7 +568,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* Inductive types: MutInd MutConstruct Fix Cofix *) | (FInd (ind1,u1 as pind1), FInd (ind2,u2 as pind2)) -> - if eq_ind ind1 ind2 then + if Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -588,7 +588,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | (FConstruct ((ind1,j1),u1 as pctor1), FConstruct ((ind2,j2),u2 as pctor2)) -> - if Int.equal j1 j2 && eq_ind ind1 ind2 then + if Int.equal j1 j2 && Ind.CanOrd.equal ind1 ind2 then if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then let cuniv = convert_instances ~flex:false u1 u2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -669,7 +669,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible | FCaseInvert (ci1,p1,_,_,br1,e1), FCaseInvert (ci2,p2,_,_,br2,e2) -> - (if not (eq_ind ci1.ci_ind ci2.ci_ind) then raise NotConvertible); + (if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible); let el1 = el_stack lft1 v1 and el2 = el_stack lft2 v2 in let ccnv = ccnv CONV l2r infos el1 el2 in let cuniv = ccnv (mk_clos e1 p1) (mk_clos e2 p2) cuniv in @@ -704,14 +704,14 @@ and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv = | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> - if not (Projection.Repr.equal c1 c2) then + if not (Projection.Repr.CanOrd.equal c1 c2) then raise NotConvertible else cu1 | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> let cu2 = f fx1 fx2 cu1 in cmp_rec a1 a2 cu2 | (Zlcase(ci1,l1,p1,br1,e1),Zlcase(ci2,l2,p2,br2,e2)) -> - if not (eq_ind ci1.ci_ind ci2.ci_ind) then + if not (Ind.CanOrd.equal ci1.ci_ind ci2.ci_ind) then raise NotConvertible; let cu2 = f (l1, mk_clos e1 p1) (l2, mk_clos e2 p2) cu1 in convert_branches l2r infos ci1 e1 e2 l1 l2 br1 br2 cu2 |