Adapt to coq/coq#18280 (case relevance outside case info)

SkySkimmer · Nov 9, 2023 · dc337c2 · dc337c2
1 parent a333601
commit dc337c2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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