From 01d0b60694e3b4ee810bdde7115b40e49355ac24 Mon Sep 17 00:00:00 2001
From: Michael Soegtrop
Date: Tue, 18 Jun 2019 21:01:27 +0200
Subject: Removed "b" from function names in Bool.v Changed year in headers

---
 user-contrib/Ltac2/Bool.v   | 14 +++++++-------
 user-contrib/Ltac2/List.v   |  4 ++--
 user-contrib/Ltac2/Option.v |  2 +-
 3 files changed, 10 insertions(+), 10 deletions(-)
 mode change 100644 => 100755 user-contrib/Ltac2/Bool.v

diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v
old mode 100644
new mode 100755
index 413746acbd..d808436e13
--- a/user-contrib/Ltac2/Bool.v
+++ b/user-contrib/Ltac2/Bool.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -10,31 +10,31 @@
 
 Require Import Ltac2.Init.
 
-Ltac2 andb x y :=
+Ltac2 and x y :=
   match x with
   | true => y
   | false => false
   end.
 
-Ltac2 orb x y :=
+Ltac2 or x y :=
   match x with
   | true => true
   | false => y
   end.
 
-Ltac2 implb x y :=
+Ltac2 impl x y :=
   match x with
   | true => y
   | false => true
   end.
 
-Ltac2 negb x :=
+Ltac2 neg x :=
   match x with
   | true => false
   | false => true
   end.
 
-Ltac2 xorb x y :=
+Ltac2 xor x y :=
   match x with
   | true
     => match y with
@@ -48,7 +48,7 @@ Ltac2 xorb x y :=
        end
   end.
 
-Ltac2 eqb x y :=
+Ltac2 eq x y :=
   match x with
   | true
     => match y with
diff --git a/user-contrib/Ltac2/List.v b/user-contrib/Ltac2/List.v
index 07505d7d54..3783618cb1 100644
--- a/user-contrib/Ltac2/List.v
+++ b/user-contrib/Ltac2/List.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
@@ -431,7 +431,7 @@ Ltac2 rec filter f xs :=
   end.
 
 Ltac2 rec filter_out f xs :=
-  filter (fun x => Bool.negb (f x)) xs.
+  filter (fun x => Bool.neg (f x)) xs.
 
 Ltac2 find_all (f : 'a -> bool) (ls : 'a list) := filter f ls.
 
diff --git a/user-contrib/Ltac2/Option.v b/user-contrib/Ltac2/Option.v
index 0f09a0cc48..af0b7c28ca 100644
--- a/user-contrib/Ltac2/Option.v
+++ b/user-contrib/Ltac2/Option.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
 (* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
 (*    //   *    This file is distributed under the terms of the         *)
-- 
cgit v1.2.3