From ad818794f5d0c08c116e5c7f5995167c9e2a658c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 10 Nov 2023 14:45:51 +0100 Subject: [PATCH] Adapt to coq/coq#18280 (case relevance outside case info) --- src/Language/IdentifierParameters.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v index 07d87c33cd..5cb0581bdc 100644 --- a/src/Language/IdentifierParameters.v +++ b/src/Language/IdentifierParameters.v @@ -11,6 +11,7 @@ Import Ltac2.Constr.Unsafe. Require Rewriter.Util.InductiveHList. Require Rewriter.Util.LetIn. Import InductiveHList.Notations. +Require Import Rewriter.Util.Tactics2.DestCase. Require Import Ltac2.Printf. (* TODO: move to Util *) @@ -28,8 +29,9 @@ Ltac2 Set reify_preprocess_extra := => let t := Constr.type term in '(@ZRange.zrange_rect_nodep $t $f $x) *) match Constr.Unsafe.kind term with - | Constr.Unsafe.Case cinfo ret_ty cinv x branches - => match Constr.Unsafe.kind ret_ty with + | Constr.Unsafe.Case _ _ _ _ _ + => let (cinfo, ret_ty, cinv, x, branches) := destCase term in + match Constr.Unsafe.kind ret_ty with | Constr.Unsafe.Lambda xb ret_ty => let ty := Constr.Unsafe.substnl [x] 0 ret_ty in lazy_match! Constr.Binder.type xb with