From dbd992f55be7116450e95c4e45b822eb38c18606 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 9 Nov 2023 16:49:06 +0100 Subject: [PATCH] Adapt to coq/coq#18280 (case relevance outside case info) --- serlib/ser_constr.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/serlib/ser_constr.ml b/serlib/ser_constr.ml index db5d44bf..65289d45 100644 --- a/serlib/ser_constr.ml +++ b/serlib/ser_constr.ml @@ -151,8 +151,8 @@ let rec _constr_put (c : Constr.t) : _constr = | C.Const p -> Const p | C.Ind(p,q) -> Ind (p,q) | C.Construct(p) -> Construct (p) - | C.Case(ci, u, ca, pr, pi, c, pb) -> - Case(ci, u, cra ca, crcr pr, crci pi, cr c, Array.map crcb pb) + | C.Case(ci, u, ca, (pr,r), pi, c, pb) -> + Case(ci, u, cra ca, (crcr pr,r), crci pi, cr c, Array.map crcb pb) (* (int array * int) * (Name.t array * 'types array * 'constr array)) *) | C.Fix(p,(na,u1,u2)) -> Fix(p, (na, cra u1, cra u2)) | C.CoFix(p,(na,u1,u2)) -> CoFix(p, (na, cra u1, cra u2)) @@ -183,7 +183,7 @@ let rec _constr_get (c : _constr) : Constr.t = | Const p -> C.mkConstU(p) | Ind(p,q) -> C.mkIndU(p, q) | Construct(p) -> C.mkConstructU(p) - | Case(ci, u, ca, pr, pi, c, pb) -> C.mkCase (ci, u, cra ca, crcr pr, crci pi, cr c, Array.map crcb pb) + | Case(ci, u, ca, (pr,r), pi, c, pb) -> C.mkCase (ci, u, cra ca, (crcr pr,r), crci pi, cr c, Array.map crcb pb) | Fix (p,(na,u1,u2)) -> C.mkFix(p, (na, cra u1, cra u2)) | CoFix(p,(na,u1,u2)) -> C.mkCoFix(p, (na, cra u1, cra u2)) | Proj(p,r,c) -> C.mkProj(p, r, cr c)