Merge PR coq#19399: done with simple refine

Reviewed-by: gares Co-authored-by: gares <[email protected]>
SkySkimmer · Jul 22, 2024 · 4b52a0d · 4b52a0d
2 parents 7fa961b + 02820a7
commit 4b52a0d
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/doc/changelog/07-ssreflect/19399-done_with_simple_refine.rst b/doc/changelog/07-ssreflect/19399-done_with_simple_refine.rst
@@ -0,0 +1,2 @@
+- **Changed:**
+  `done` uses `simple refine` instead of `apply` to apply `sym_equal`
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
@@ -395,7 +395,7 @@ Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
 (**  The basic closing tactic "done".  **)
 Ltac done :=
   trivial; hnf; intros; solve
-   [ do ![solve [trivial | apply: (@sym_equal _ _ _ _); trivial]
+   [ do ![solve [trivial | simple refine (@sym_equal _ _ _ _); trivial]
          | discriminate | contradiction | split]
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		- Changed:
		`done` uses `simple refine` instead of `apply` to apply `sym_equal`