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

mit-plv · Nov 14, 2023 · 6551f87 · 6551f87
1 parent df6436e
commit 6551f87
Showing 1 changed file with 3 additions and 5 deletions.
diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v
@@ -46,13 +46,11 @@ Ltac2 Set reify_preprocess_extra :=
          end
      end.
 
+Local Ltac2 Notation "red_flags:(" s(strategy) ")" := s.
+
 (* TODO: Move to util *)
 Ltac2 eval_cbv_beta (c : constr) :=
-  Std.eval_cbv { Std.rBeta := true; Std.rMatch := false;
-                 Std.rFix := false; Std.rCofix := false;
-                 Std.rZeta := false; Std.rDelta := false;
-                 Std.rConst := [] }
-               c.
+  Std.eval_cbv (red_flags:(beta)) c.
 
 Ltac2 Set reify_ident_preprocess_extra :=
   fun ctx_tys term