Merge PR coq#19102: Ltac2: Avoid double typechecking in exact

Reviewed-by: ppedrot Co-authored-by: ppedrot <[email protected]>
SkySkimmer · Jun 11, 2024 · b57e3f4 · b57e3f4
2 parents 58d8ec3 + 3ed0133
commit b57e3f4
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/user-contrib/Ltac2/Notations.v b/user-contrib/Ltac2/Notations.v
@@ -483,7 +483,7 @@ Ltac2 exact1 ev c :=
         (Constr.Pretype.expected_oftype (Control.goal()))
         c
     in
-    Control.refine (fun _ => c)).
+    Std.exact_no_check c).
 
 Ltac2 Notation "exact" c(preterm) := exact1 false c.