From 47d241b581c7966a94726648d5e43bd9a92b9fa3 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Nov 2023 10:51:03 -0800 Subject: [PATCH] Parenthesize red_flags --- src/Language/IdentifierParameters.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v index 105dcd22f6b..66aa4b36bc0 100644 --- a/src/Language/IdentifierParameters.v +++ b/src/Language/IdentifierParameters.v @@ -50,7 +50,7 @@ Local Ltac2 Notation "red_flags:(" s(strategy) ")" := s. (* TODO: Move to util *) Ltac2 eval_cbv_beta (c : constr) := - Std.eval_cbv red_flags:(beta) c. + Std.eval_cbv (red_flags:(beta)) c. Ltac2 Set reify_ident_preprocess_extra := fun ctx_tys term