From dc337c2e4d7e006b139c831f15c7d8f92361f0f7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Thu, 9 Nov 2023 16:53:49 +0100 Subject: [PATCH] Adapt to coq/coq#18280 (case relevance outside case info) --- src/wp_rewrite.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/wp_rewrite.ml b/src/wp_rewrite.ml index 2889b2d9..7d058dda 100644 --- a/src/wp_rewrite.ml +++ b/src/wp_rewrite.ml @@ -164,7 +164,7 @@ end = struct | Construct (c,u) -> Some (DRef (ConstructRef c), []) | Meta _ -> assert false | Evar (i,_) -> None - | Case (ci,u1,pms1,c1,_iv,c2,ca) -> Some (DCase(ci), [snd c1; c2] @ Array.map_to_list snd ca) + | Case (ci,u1,pms1,(c1,_),_iv,c2,ca) -> Some (DCase(ci), [snd c1; c2] @ Array.map_to_list snd ca) | Fix ((ia,i),(_,ta,ca)) -> Some (DFix(ia,i), Array.to_list ta @ Array.to_list ca) | CoFix (i,(_,ta,ca)) -> Some (DCoFix(i), Array.to_list ta @ Array.to_list ca) | Cast (c,_,_) -> pat_of_constr c