From 8cdabbb14370b4b880faa5eb39637b4b38bc757d Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Mon, 12 Sep 2022 16:59:08 +0200
Subject: [PATCH] [Extlib] removed xor
---
bin/migration_scripts/manganese2iron.sh | 3 ++-
src/kernel_internals/typing/mergecil.ml | 2 +-
src/libraries/stdlib/extlib.ml | 6 ------
src/libraries/stdlib/extlib.mli | 8 --------
4 files changed, 3 insertions(+), 16 deletions(-)
diff --git a/bin/migration_scripts/manganese2iron.sh b/bin/migration_scripts/manganese2iron.sh
index 2f6fda59997..9af1cd289a6 100755
--- a/bin/migration_scripts/manganese2iron.sh
+++ b/bin/migration_scripts/manganese2iron.sh
@@ -86,7 +86,8 @@ process_file ()
fi
sedi "$file" \
-e 's/Extlib\.id/Fun.id/g' \
- -e 's/Extlib\.swap/Fun.flip/g'
+ -e 's/Extlib\.swap/Fun.flip/g' \
+ -e 's/Extlib\.xor/(<>)/g'
# this line left empty on purpose
}
diff --git a/src/kernel_internals/typing/mergecil.ml b/src/kernel_internals/typing/mergecil.ml
index d962659e2cc..9f6b3b97c10 100644
--- a/src/kernel_internals/typing/mergecil.ml
+++ b/src/kernel_internals/typing/mergecil.ml
@@ -2671,7 +2671,7 @@ let oneFilePass2 (f: file) =
visit vi';
vi'.vaddrof <- vi.vaddrof || vi'.vaddrof;
vi'.vdefined <- vi.vdefined || vi'.vdefined;
- if Extlib.xor vi'.vghost vi.vghost then
+ if vi'.vghost <> vi.vghost then
Kernel.abort
"Cannot merge: Global %a has both ghost and non-ghost status"
Cil_printer.pp_varinfo vi';
diff --git a/src/libraries/stdlib/extlib.ml b/src/libraries/stdlib/extlib.ml
index 0ce56cce839..1aaa77b0c04 100644
--- a/src/libraries/stdlib/extlib.ml
+++ b/src/libraries/stdlib/extlib.ml
@@ -242,12 +242,6 @@ let opt_map2 f x y = match x, y with
| None, _ | _, None -> None
| Some x, Some y -> Some (f x y)
-(* ************************************************************************* *)
-(** Booleans *)
-(* ************************************************************************* *)
-
-let xor x y = if x then not y else y
-
(* ************************************************************************* *)
(** {2 Performance} *)
(* ************************************************************************* *)
diff --git a/src/libraries/stdlib/extlib.mli b/src/libraries/stdlib/extlib.mli
index c641d93e5f3..0335824ac57 100644
--- a/src/libraries/stdlib/extlib.mli
+++ b/src/libraries/stdlib/extlib.mli
@@ -207,14 +207,6 @@ val opt_map2: ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option
[None].
@since 24.0-Chromium *)
-(* ************************************************************************* *)
-(** {2 Booleans} *)
-(* ************************************************************************* *)
-
-val xor: bool -> bool -> bool
-(** exclusive-or.
- @since Oxygen-20120901 *)
-
(* ************************************************************************* *)
(** {2 Strings} *)
(* ************************************************************************* *)
--
GitLab