[ssr] Remove no longer used not_locked_false_eq_true

Alizter · Jul 19, 2024 · de8f034 · de8f034
1 parent 11308c2
commit de8f034
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 11 deletions.
diff --git a/doc/changelog/07-ssreflect/19382-ssr_rm_not_locked_false_eq_true.rst b/doc/changelog/07-ssreflect/19382-ssr_rm_not_locked_false_eq_true.rst
@@ -0,0 +1,5 @@
+- **Removed:**
+  no longer used lemma ``not_locked_false_eq_true``
+  and its call in the :tacn:`done` tactic
+  (`#19382 <https://github.com/coq/coq/pull/19382>`_,
+  by Pierre Roux).
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2155,13 +2155,11 @@ with a ``by``, like in:
         trivial; hnf; intros; solve
          [ do ![solve [trivial | apply: sym_equal; trivial]
                | discriminate | contradiction | split]
-         | case not_locked_false_eq_true; assumption
          | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
-   The lemma :g:`not_locked_false_eq_true` is needed to discriminate
-   *locked* boolean predicates (see Section :ref:`locking_ssr`). The iterator
-   tactical ``do`` is presented in Section :ref:`iteration_ssr`. This tactic can be
-   customized by the user, for instance to include an :tacn:`auto` tactic.
+   The iterator tactical ``do`` is presented in Section
+   :ref:`iteration_ssr`. This tactic can be customized by the user,
+   for instance to include an :tacn:`auto` tactic.
 
 A natural and common way of closing a goal is to apply a lemma that
 is the exact one needed for the goal to be solved. The defective form

diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
@@ -392,24 +392,18 @@ Register locked as plugins.ssreflect.locked.
 
 Lemma lock A x : x = locked x :> A. Proof. unlock; reflexivity. Qed.
 
-(**  Needed for locked predicates, in particular for eqType's.  **)
-Lemma not_locked_false_eq_true : locked false <> true.
-Proof. unlock; discriminate. Qed.
-
 (**  The basic closing tactic "done".  **)
 Ltac done :=
   trivial; hnf; intros; solve
    [ do ![solve [trivial | apply: sym_equal; trivial]
          | discriminate | contradiction | split]
-   | case not_locked_false_eq_true; assumption
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
 (**  Quicker done tactic not including split, syntax: /0/  **)
 Ltac ssrdone0 :=
   trivial; hnf; intros; solve
    [ do ![solve [trivial | apply: sym_equal; trivial]
          | discriminate | contradiction ]
-   | case not_locked_false_eq_true; assumption
    | match goal with H : ~ _ |- _ => solve [case H; trivial] end ].
 
 (**  To unlock opaque constants.  **)