diff options
| -rw-r--r-- | checker/reduction.ml | 12 | ||||
| -rw-r--r-- | test-suite/coqchk/include_primproj.v | 13 |
2 files changed, 21 insertions, 4 deletions
diff --git a/checker/reduction.ml b/checker/reduction.ml index ae15a36d57..d36c0ef2c9 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -133,7 +133,7 @@ let convert_universes univ u u' = if Univ.Instance.check_eq univ u u' then () else raise NotConvertible -let compare_stacks f fmind lft1 stk1 lft2 stk2 = +let compare_stacks f fmind fproj lft1 stk1 lft2 stk2 = let rec cmp_rec pstk1 pstk2 = match (pstk1,pstk2) with | (z1::s1, z2::s2) -> @@ -143,8 +143,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Names.Projection.Repr.UserOrd.equal c1 c2) then - raise NotConvertible + if not (fproj c1 c2) then + raise NotConvertible | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) -> if not (fmind ci1.ci_ind ci2.ci_ind) then raise NotConvertible; @@ -298,6 +298,10 @@ let eq_table_key univ = Constant.UserOrd.equal c1 c2 && Univ.Instance.check_eq univ u1 u2) +let proj_equiv_infos infos p1 p2 = + Int.equal (Projection.Repr.arg p1) (Projection.Repr.arg p2) && + mind_equiv (infos_env infos) (Projection.Repr.inductive p1) (Projection.Repr.inductive p2) + (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 = eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[])) @@ -521,7 +525,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) = and convert_stacks univ infos lft1 lft2 stk1 stk2 = compare_stacks (fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2) - (mind_equiv_infos infos) + (mind_equiv_infos infos) (proj_equiv_infos infos) lft1 stk1 lft2 stk2 and convert_vect univ infos lft1 lft2 v1 v2 = diff --git a/test-suite/coqchk/include_primproj.v b/test-suite/coqchk/include_primproj.v new file mode 100644 index 0000000000..804ba1d378 --- /dev/null +++ b/test-suite/coqchk/include_primproj.v @@ -0,0 +1,13 @@ +(* #7329 *) +Set Primitive Projections. + +Module M. + Module Bar. + Record Box := box { unbox : Type }. + + Axiom foo : Box. + Axiom baz : forall _ : unbox foo, unbox foo. + End Bar. +End M. + +Include M. |