diff options
| author | Gaëtan Gilbert | 2018-04-22 17:26:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-24 13:49:18 +0200 |
| commit | a30be8ca7d6b7c6f17aa65de824e02194a7f3a9b (patch) | |
| tree | 9b43febeca66aa4e8914ac90f9089f87f090da6c /checker | |
| parent | 0108db19c96e1b46346f032964f2cca3f8149cb3 (diff) | |
Fix #7329: coqchk Include with primitive projections
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/reduction.ml | 12 |
1 files changed, 8 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 = |