Adapt to coq/coq#18273 (Ltac2 supports head reduction) (#102)

mit-plv · Nov 8, 2023 · a80d8c2 · a80d8c2
1 parent e680a0d
commit a80d8c2
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 26 deletions.
diff --git a/src/coqutil/Datatypes/RecordSetters.v b/src/coqutil/Datatypes/RecordSetters.v
@@ -155,6 +155,7 @@ Require Import Ltac2.Ltac2.
 Require Ltac2.Option.
 Require Import Ltac2.Bool.
 Require coqutil.Ltac2Lib.Constr.
+Require Import coqutil.Ltac2Lib.Std.
 
 Set Default Proof Mode "Classic".
 
@@ -212,16 +213,7 @@ Module record.
                         end in
     match Constr.Unsafe.kind h with
     | Constr.Unsafe.Constant cst _ =>
-        let flags := {
-            Std.rBeta := false;
-            Std.rMatch := false;
-            Std.rFix := false;
-            Std.rCofix := false;
-            Std.rZeta := false;
-            Std.rDelta := false; (* false = delta only on rConst*)
-            Std.rConst := [Std.ConstRef cst]
-          } in
-        let unfolded_h := Std.eval_cbv flags h in
+        let unfolded_h := eval_cbv_delta [Std.ConstRef cst] h in
         match strip_n_lambdas nparams unfolded_h with
         | Some l => unfolded_getter_proj_index l
         | None => None

diff --git a/src/coqutil/Datatypes/RecordSettersUsingExistingGetters.v b/src/coqutil/Datatypes/RecordSettersUsingExistingGetters.v
@@ -12,6 +12,7 @@ Require Import Ltac2.Ltac2.
 Require Import Ltac2.Bool.
 Require Import coqutil.Ltac2Lib.Constr.
 Require coqutil.Ltac2Lib.List.
+Require Import coqutil.Ltac2Lib.Std.
 Require Import coqutil.Tactics.RecordEta.
 Set Default Proof Mode "Classic".
 
@@ -162,16 +163,7 @@ Module record.
                         end in
     match Constr.Unsafe.kind h with
     | Constr.Unsafe.Constant cst _ =>
-        let flags := {
-            Std.rBeta := false;
-            Std.rMatch := false;
-            Std.rFix := false;
-            Std.rCofix := false;
-            Std.rZeta := false;
-            Std.rDelta := false; (* false = delta only on rConst*)
-            Std.rConst := [Std.ConstRef cst]
-          } in
-        let unfolded_h := Std.eval_cbv flags h in
+        let unfolded_h := eval_cbv_delta [Std.ConstRef cst] h in
         match strip_n_lambdas nparams unfolded_h with
         | Some l => unfolded_getter_proj_index l
         | None => None

diff --git a/src/coqutil/Ltac2Lib/Std.v b/src/coqutil/Ltac2Lib/Std.v
@@ -1,16 +1,14 @@
 Require Import Ltac2.Ltac2 Ltac2.Std.
 Require Import coqutil.Ltac2Lib.Pervasives.
 
+Local Ltac2 Notation "red_flags" s(strategy) := s.
+
 (* Beware: Ltac2's Std.eval_cbv does not match Ltac1's `eval cbv in`!
    https://github.com/coq/coq/issues/14303 *)
 Ltac2 eval_cbv_delta(refs: reference list)(e: constr): constr :=
-  eval_cbv {
+  (* compat: rStrength is >=8.19 only *)
+  eval_cbv { (red_flags beta) with
      rBeta := false;
-     rMatch := false;
-     rFix := false;
-     rCofix := false;
-     rZeta := false;
-     rDelta := false; (* false = delta only on rConst*)
      rConst := refs
   } e.