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

mit-plv · Nov 13, 2023 · 05d903f · 05d903f
1 parent dcd5678
commit 05d903f
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