diff options
| -rwxr-xr-x[-rw-r--r--] | user-contrib/Ltac2/Bool.v | 14 | ||||
| -rw-r--r-- | user-contrib/Ltac2/List.v | 4 | ||||
| -rw-r--r-- | user-contrib/Ltac2/Option.v | 2 |
3 files changed, 10 insertions, 10 deletions
diff --git a/user-contrib/Ltac2/Bool.v b/user-contrib/Ltac2/Bool.v index 413746acbd..d808436e13 100644..100755 --- 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 *) |