diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v index 5cb0581bdc..66aa4b36bc 100644 --- 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