From e27fdd18cdfd8424d19058a3b59256219d111733 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 17 Apr 2021 20:08:36 +0200
Subject: 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.
---
 user-contrib/Ltac2/Bool.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'user-contrib')

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.
-- 
cgit v1.2.3