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

.gitignore

@@ -122,6 +122,7 @@ src/Rewriter/Util/plugins/ltac2_extra_plugin.mlg
 src/Rewriter/Util/plugins/ltac2_extra_plugin.mllib
 
 src/Rewriter/Util/Tactics2/Constr.v
+src/Rewriter/Util/Tactics2/DestCase.v
 src/Rewriter/Util/Tactics2/DestProj.v
 src/Rewriter/Util/Tactics2/Proj.v
 

Makefile.local.common

@@ -64,6 +64,7 @@ COMPATIBILITY_FILES := \
 	src/Rewriter/Util/plugins/StrategyTactic.v \
 	src/Rewriter/Util/plugins/Ltac2Extra.v \
 	src/Rewriter/Util/Tactics2/Constr.v \
+	src/Rewriter/Util/Tactics2/DestCase.v \
 	src/Rewriter/Util/Tactics2/DestProj.v \
 	src/Rewriter/Util/Tactics2/Proj.v \
 	#

src/Rewriter/Language/Reify.v

@@ -32,6 +32,7 @@ Require Rewriter.Util.Tactics2.Ident.
 Require Rewriter.Util.Tactics2.String.
 Require Rewriter.Util.Tactics2.Constr.
 Require Import Rewriter.Util.Tactics2.DestEvar.
+Require Import Rewriter.Util.Tactics2.DestCase.
 Require Import Rewriter.Util.Tactics2.InstantiateEvar.
 Require Import Rewriter.Util.Tactics2.Constr.Unsafe.MakeAbbreviations.
 Require Import Rewriter.Util.Tactics2.FixNotationsForPerformance.
@@ -510,8 +511,9 @@ Module Compilers.
                       reify_preprocess v
                   end
            end
-      | Constr.Unsafe.Case cinfo ret_ty cinv x branches
+      | Constr.Unsafe.Case _ _ _ _ _
         => Reify.debug_enter_reify_case "expr.reify_preprocess" "Case" term;
+           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

src/Rewriter/Util/Tactics2/Constr.v.v819

@@ -51,7 +51,7 @@ Module Unsafe.
     | Case _ x iv y bl
       => Array.iter f bl;
          Case.iter_invert f iv;
-         f x;
+         match x with (x,_) => f x end;
          f y
     | Proj _p _ c => f c
     | Fix _ _ tl bl =>
@@ -82,7 +82,7 @@ Module Unsafe.
     | Case _ x iv y bl
       => Array.iter (f n) bl;
          Case.iter_invert (f n) iv;
-         f n x;
+         match x with (x,_) => f n x end;
          f n y
     | Proj _p _ c => f n c
     | Fix _ _ tl bl =>

src/Rewriter/Util/Tactics2/DestCase.v.v815

@@ -0,0 +1 @@
+DestCase.v.v818

src/Rewriter/Util/Tactics2/DestCase.v.v816

@@ -0,0 +1 @@
+DestCase.v.v818

src/Rewriter/Util/Tactics2/DestCase.v.v817

@@ -0,0 +1 @@
+DestCase.v.v818

src/Rewriter/Util/Tactics2/DestCase.v.v819

@@ -0,0 +1,11 @@
+Require Import Ltac2.Ltac2.
+Require Export Rewriter.Util.FixCoqMistakes.
+Import Ltac2.Constr.Unsafe.
+
+Ltac2 Type exn ::= [ Not_a_case (kind) ].
+Ltac2 destCase (c : constr) :=
+  let k := kind c in
+  match k with
+  | Case a b c d e => let (b,_) := b in (a, b, c, d, e)
+  | _ => Control.throw (Not_a_case k)
+  end.