Uniformize the name of the Ltac2 boolean equality function.

All other equality functions are called "equal" but this one was called "eq".
We add a deprecated alias for backward compatibility.

1 files changed, 4 insertions, 1 deletions

diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
index 624097728e..b201574808 100644
--- a/user-contrib/Ltac2/Bool.v
+++ b/user-contrib/Ltac2/Bool.v
@@ -48,7 +48,7 @@ Ltac2 xor x y :=
        end
   end.
 
-Ltac2 eq x y :=
+Ltac2 equal x y :=
   match x with
   | true
     => match y with
@@ -61,3 +61,6 @@ Ltac2 eq x y :=
        | false => true
        end
   end.
+
+#[deprecated(note="Use Bool.equal", since="8.14")]
+Ltac2 eq := equal.