From 5d08cca6fc0cb790200f816f14b78ab61921d72b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 21 Apr 2021 23:18:28 +0200
Subject: [PATCH] Check headers
---
Makefile | 59 ++++++++++++-------
misc/header_colibri2.txt | 17 ++++++
misc/header_colibrics.txt | 2 +-
misc/header_witan.txt | 2 +-
src_colibri2/bin/main.ml | 20 +++++++
src_colibri2/bin/options.ml | 22 +++++++
src_colibri2/core/colibri2_core.ml | 4 +-
src_colibri2/core/datastructure.ml | 4 +-
src_colibri2/core/datastructure.mli | 4 +-
src_colibri2/core/demon.ml | 4 +-
src_colibri2/core/demon.mli | 4 +-
src_colibri2/core/egraph.ml | 4 +-
src_colibri2/core/egraph.mli | 4 +-
src_colibri2/core/env.ml | 4 +-
src_colibri2/core/env.mli | 4 +-
src_colibri2/core/events.ml | 4 +-
src_colibri2/core/events.mli | 4 +-
src_colibri2/core/ground.ml | 20 +++++++
src_colibri2/core/ground.mli | 20 +++++++
src_colibri2/core/interp.ml | 4 +-
src_colibri2/core/interp.mli | 4 +-
src_colibri2/core/structures/domKind.ml | 4 +-
src_colibri2/core/structures/domKind.mli | 4 +-
src_colibri2/core/structures/expr.ml | 20 +++++++
src_colibri2/core/structures/nodes.ml | 4 +-
src_colibri2/core/structures/nodes.mli | 4 +-
src_colibri2/core/structures/term.ml | 4 +-
src_colibri2/core/theory.ml | 4 +-
src_colibri2/popop_lib/IArray.ml | 4 +-
src_colibri2/popop_lib/IArray.mli | 4 +-
src_colibri2/popop_lib/TimeWheel.ml | 20 +++++++
src_colibri2/popop_lib/TimeWheel.mli | 20 +++++++
src_colibri2/popop_lib/enum.ml | 4 +-
src_colibri2/popop_lib/enum.mli | 4 +-
src_colibri2/popop_lib/popop_stdlib.ml | 29 ++++-----
src_colibri2/popop_lib/popop_stdlib.mli | 29 ++++-----
src_colibri2/popop_lib/refo.ml | 4 +-
src_colibri2/popop_lib/refo.mli | 4 +-
src_colibri2/popop_lib/simple_vector.ml | 4 +-
src_colibri2/popop_lib/simple_vector.mli | 4 +-
src_colibri2/popop_lib/unit.ml | 4 +-
src_colibri2/popop_lib/unit.mli | 4 +-
src_colibri2/popop_lib/vector_hetero.ml | 4 +-
src_colibri2/popop_lib/vector_hetero.mli | 4 +-
src_colibri2/solver/input.ml | 4 +-
src_colibri2/solver/scheduler.ml | 4 +-
src_colibri2/solver/scheduler.mli | 4 +-
src_colibri2/solver/solver.ml | 4 +-
src_colibri2/stdlib/comp_keys.ml | 7 ++-
src_colibri2/stdlib/comp_keys.mli | 4 +-
src_colibri2/stdlib/config.ml | 4 +-
src_colibri2/stdlib/context.ml | 4 +-
src_colibri2/stdlib/context.mli | 4 +-
src_colibri2/stdlib/hashtbl_hetero.ml | 4 +-
src_colibri2/stdlib/hashtbl_hetero.mli | 4 +-
src_colibri2/stdlib/hashtbl_hetero_sig.ml | 4 +-
src_colibri2/stdlib/keys.ml | 4 +-
src_colibri2/stdlib/keys.mli | 4 +-
src_colibri2/stdlib/keys_sig.ml | 4 +-
src_colibri2/stdlib/map_hetero.ml | 4 +-
src_colibri2/stdlib/map_hetero.mli | 4 +-
src_colibri2/stdlib/map_hetero_sig.ml | 4 +-
src_colibri2/stdlib/shuffle.ml | 4 +-
src_colibri2/stdlib/shuffle.mli | 4 +-
src_colibri2/stdlib/std.ml | 4 +-
src_colibri2/stdlib/std.mli | 4 +-
src_colibri2/stdlib/std_sig.ml | 4 +-
src_colibri2/stdlib/wto.ml | 40 ++++++-------
src_colibri2/stdlib/wto.mli | 40 ++++++-------
.../generate_tests/generate_dune_tests.ml | 20 +++++++
src_colibri2/tests/test.ml | 4 +-
src_colibri2/tests/tests.ml | 4 +-
src_colibri2/tests/tests_LRA.ml | 4 +-
src_colibri2/tests/tests_bool.ml | 4 +-
src_colibri2/tests/tests_lib.ml | 4 +-
src_colibri2/tests/tests_uf.ml | 4 +-
src_colibri2/theories/ADT/adt.ml | 20 +++++++
src_colibri2/theories/ADT/adt.mli | 20 +++++++
src_colibri2/theories/ADT/adt_value.ml | 20 +++++++
src_colibri2/theories/ADT/adt_value.mli | 20 +++++++
src_colibri2/theories/LRA/LRA.ml | 4 +-
src_colibri2/theories/LRA/LRA.mli | 4 +-
src_colibri2/theories/LRA/delta.ml | 20 +++++++
src_colibri2/theories/LRA/delta.mli | 20 +++++++
src_colibri2/theories/LRA/dom_interval.ml | 4 +-
src_colibri2/theories/LRA/dom_interval.mli | 20 +++++++
src_colibri2/theories/LRA/dom_polynome.ml | 4 +-
src_colibri2/theories/LRA/dom_polynome.mli | 4 +-
src_colibri2/theories/LRA/dom_product.ml | 4 +-
src_colibri2/theories/LRA/dom_product.mli | 4 +-
src_colibri2/theories/LRA/fourier.ml | 20 +++++++
src_colibri2/theories/LRA/fourier.mli | 20 +++++++
.../theories/LRA/integer_sign_domain.ml | 40 ++++++-------
.../theories/LRA/integer_sign_domain.mli | 20 +++++++
src_colibri2/theories/LRA/interval.ml | 4 +-
src_colibri2/theories/LRA/interval.mli | 4 +-
src_colibri2/theories/LRA/interval_sig.ml | 4 +-
src_colibri2/theories/LRA/mul.ml | 20 +++++++
src_colibri2/theories/LRA/mul.mli | 20 +++++++
src_colibri2/theories/LRA/polynome.ml | 4 +-
src_colibri2/theories/LRA/polynome.mli | 4 +-
src_colibri2/theories/LRA/product.ml | 4 +-
src_colibri2/theories/LRA/product.mli | 4 +-
src_colibri2/theories/LRA/realValue.ml | 4 +-
src_colibri2/theories/LRA/realValue.mli | 4 +-
src_colibri2/theories/LRA/sign_domain.ml | 40 ++++++-------
src_colibri2/theories/LRA/sign_domain.mli | 20 +++++++
src_colibri2/theories/bool/boolean.ml | 4 +-
src_colibri2/theories/bool/boolean.mli | 4 +-
src_colibri2/theories/bool/equality.ml | 4 +-
src_colibri2/theories/bool/equality.mli | 4 +-
src_colibri2/theories/quantifier/F.ml | 20 +++++++
src_colibri2/theories/quantifier/FA.ml | 20 +++++++
src_colibri2/theories/quantifier/F_Pos.ml | 20 +++++++
src_colibri2/theories/quantifier/F_Pos.mli | 20 +++++++
.../theories/quantifier/InvertedPath.ml | 20 +++++++
.../theories/quantifier/InvertedPath.mli | 20 +++++++
src_colibri2/theories/quantifier/PC.ml | 20 +++++++
src_colibri2/theories/quantifier/PC.mli | 20 +++++++
src_colibri2/theories/quantifier/PN.ml | 20 +++++++
src_colibri2/theories/quantifier/PN.mli | 20 +++++++
src_colibri2/theories/quantifier/PP.ml | 20 +++++++
src_colibri2/theories/quantifier/PP.mli | 20 +++++++
src_colibri2/theories/quantifier/common.ml | 20 +++++++
src_colibri2/theories/quantifier/info.ml | 20 +++++++
src_colibri2/theories/quantifier/info.mli | 20 +++++++
src_colibri2/theories/quantifier/pattern.ml | 20 +++++++
src_colibri2/theories/quantifier/pattern.mli | 20 +++++++
.../theories/quantifier/quantifier.ml | 20 +++++++
.../theories/quantifier/quantifier.mli | 20 +++++++
src_colibri2/theories/quantifier/trigger.ml | 20 +++++++
src_colibri2/theories/quantifier/trigger.mli | 20 +++++++
src_colibri2/theories/quantifier/uninterp.ml | 4 +-
src_colibri2/theories/quantifier/uninterp.mli | 4 +-
134 files changed, 1161 insertions(+), 310 deletions(-)
create mode 100644 misc/header_colibri2.txt
diff --git a/Makefile b/Makefile
index d1cabbf78..470e3507b 100644
--- a/Makefile
+++ b/Makefile
@@ -1,12 +1,21 @@
##########################################################################
+# This file is part of Colibri2. #
# #
-# Copyright (C) 2019-2019 #
-# CEA (Commissariat à l'énergie atomique et aux énergies #
-# alternatives) #
+# Copyright (C) 2014-2021 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
# #
-# All rights reserved. #
-# Contact CEA LIST for licensing. #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
##########################################################################
all:
@@ -73,13 +82,13 @@ uninstall:
# file headers
###############
-WHY3_FILES = $(addprefix src_colibri2/popop_lib/, cmdline.ml cmdline.mli debug.ml \
- debug.mli exn_printer.ml exn_printer.mli hashcons.ml \
- hashcons.mli lists.ml lists.mli loc.ml loc.mli number.ml \
- number.mli opt.ml opt.mli plugin.ml plugin.mli pp.ml pp.mli \
- print_tree.ml print_tree.mli stdlib.ml stdlib.mli strings.ml \
- strings.mli sysutil.ml sysutil.mli util.ml util.mli \
- warning.ml warning.mli weakhtbl.ml weakhtbl.mli )
+WHY3_FILES = $(addprefix src_colibri2/popop_lib/, cmdline.ml cmdline.mli \
+ debug.ml debug.mli exn_printer.ml exn_printer.mli hashcons.ml \
+ hashcons.mli lists.ml lists.mli loc.ml loc.mli number.ml number.mli \
+ opt.ml opt.mli pp.ml pp.mli print_tree.ml print_tree.mli \
+ popop_stdlib.ml popop_stdlib.mli strings.ml strings.mli sysutil.ml \
+ sysutil.mli util.ml util.mli warning.ml warning.mli weakhtbl.ml \
+ weakhtbl.mli )
OCAML_FILES = $(addprefix src_colibri2/popop_lib/, map_intf.ml exthtbl.ml \
exthtbl.mli extmap.ml extmap.mli extset.ml extset.mli )
@@ -89,22 +98,28 @@ FRAMAC_FILES = $(addprefix src_colibri2/popop_lib/, intmap.ml intmap_hetero.ml \
JC_FILES = $(addprefix src_colibri2/popop_lib/, leftistheap.ml leftistheap.mli)
-WITAN_FILES = src_colibri2/bin/typecheck.ml src_colibri2/stdlib/std.ml src_colibri2/stdlib/std.mli \
- src_colibri2/stdlib/hashtbl_hetero.ml src_colibri2/stdlib/hashtbl_hetero.mli \
- src_colibri2/stdlib/hashtbl_hetero_sig.ml \
- src_colibri2/stdlib/map_hetero.ml src_colibri2/stdlib/map_hetero.mli \
- src_colibri2/stdlib/map_hetero_sig.ml \
- src_colibri2/stdlib/keys.mli src_colibri2/stdlib/keys_sig.ml \
- src_colibri2/stdlib/comp_keys.mli src_colibri2/stdlib/comp_keys.mli
-
-COLIBRICS_FILES = Makefile \
- $(filter-out $(WHY3_FILES) $(OCAML_FILES) $(FRAMAC_FILES) $(JC_FILES) \
+WITAN_FILES = src_colibri2/stdlib/std.ml src_colibri2/stdlib/std.mli \
+ src_colibri2/stdlib/hashtbl_hetero.ml \
+ src_colibri2/stdlib/hashtbl_hetero.mli \
+ src_colibri2/stdlib/hashtbl_hetero_sig.ml \
+ src_colibri2/stdlib/map_hetero.ml src_colibri2/stdlib/map_hetero.mli \
+ src_colibri2/stdlib/map_hetero_sig.ml src_colibri2/stdlib/keys.mli \
+ src_colibri2/stdlib/keys_sig.ml src_colibri2/stdlib/comp_keys.ml \
+ src_colibri2/stdlib/comp_keys.mli src_colibri2/bin/options.ml
+
+COLIBRI2_FILES = Makefile \
+ $(filter-out $(WHY3_FILES) $(OCAML_FILES) $(FRAMAC_FILES) $(JC_FILES) $(WITAN_FILES) \
, $(wildcard src_colibri2/*/*/*.ml* src_colibri2/*/*.ml* src_colibri2/*.ml*))
+COLIBRICS_FILES =
+
+
headers:
headache -c misc/headache_config.txt -h misc/header_colibrics.txt \
$(COLIBRICS_FILES)
headache -c misc/headache_config.txt -h misc/header_colibri2.txt \
+ $(COLIBRI2_FILES)
+ headache -c misc/headache_config.txt -h misc/header_witan.txt \
$(WITAN_FILES)
headache -c misc/headache_config.txt -h misc/header_why3.txt \
$(WHY3_FILES)
diff --git a/misc/header_colibri2.txt b/misc/header_colibri2.txt
new file mode 100644
index 000000000..743f8bbba
--- /dev/null
+++ b/misc/header_colibri2.txt
@@ -0,0 +1,17 @@
+This file is part of Colibri2.
+
+Copyright (C) 2014-2021
+ CEA (Commissariat à l'énergie atomique et aux énergies
+ alternatives)
+
+you can redistribute it and/or modify it under the terms of the GNU
+Lesser General Public License as published by the Free Software
+Foundation, version 2.1.
+
+It is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+GNU Lesser General Public License for more details.
+
+See the GNU Lesser General Public License version 2.1
+for more details (enclosed in the file licenses/LGPLv2.1).
diff --git a/misc/header_colibrics.txt b/misc/header_colibrics.txt
index 7c2e78960..bf1e8ba82 100644
--- a/misc/header_colibrics.txt
+++ b/misc/header_colibrics.txt
@@ -1,6 +1,6 @@
This file is part of Colibrics.
-Copyright (C) 2017
+Copyright (C) 2019-2021
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
diff --git a/misc/header_witan.txt b/misc/header_witan.txt
index 50a403db9..ffe19af33 100644
--- a/misc/header_witan.txt
+++ b/misc/header_witan.txt
@@ -1,6 +1,6 @@
This file is part of Colibri2.
-Copyright (C) 2017
+Copyright (C) 2017-2021
CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
INRIA (Institut National de Recherche en Informatique et en
diff --git a/src_colibri2/bin/main.ml b/src_colibri2/bin/main.ml
index 056b57e28..457225cbf 100644
--- a/src_colibri2/bin/main.ml
+++ b/src_colibri2/bin/main.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(* This file is free software, copied from dolmen. See file "LICENSE" for more information *)
let () =
diff --git a/src_colibri2/bin/options.ml b/src_colibri2/bin/options.ml
index 50396f714..f2c54316a 100644
--- a/src_colibri2/bin/options.ml
+++ b/src_colibri2/bin/options.ml
@@ -1,3 +1,25 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2017-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
(* This file is free software, part of dolmen. See file "LICENSE" for more information *)
diff --git a/src_colibri2/core/colibri2_core.ml b/src_colibri2/core/colibri2_core.ml
index 00ad7f365..f4b1d10b3 100644
--- a/src_colibri2/core/colibri2_core.ml
+++ b/src_colibri2/core/colibri2_core.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/datastructure.ml b/src_colibri2/core/datastructure.ml
index ae03ab0d6..7817ab033 100644
--- a/src_colibri2/core/datastructure.ml
+++ b/src_colibri2/core/datastructure.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/datastructure.mli b/src_colibri2/core/datastructure.mli
index 07a79d567..63cc3222a 100644
--- a/src_colibri2/core/datastructure.mli
+++ b/src_colibri2/core/datastructure.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/demon.ml b/src_colibri2/core/demon.ml
index 11bd1dacd..9e58359bf 100644
--- a/src_colibri2/core/demon.ml
+++ b/src_colibri2/core/demon.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/demon.mli b/src_colibri2/core/demon.mli
index d44791dd1..fb97f7354 100644
--- a/src_colibri2/core/demon.mli
+++ b/src_colibri2/core/demon.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/egraph.ml b/src_colibri2/core/egraph.ml
index a16452301..243c9cb65 100644
--- a/src_colibri2/core/egraph.ml
+++ b/src_colibri2/core/egraph.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/egraph.mli b/src_colibri2/core/egraph.mli
index 6cf8108ce..fbbea422c 100644
--- a/src_colibri2/core/egraph.mli
+++ b/src_colibri2/core/egraph.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/env.ml b/src_colibri2/core/env.ml
index e2722fca8..2b44678ce 100644
--- a/src_colibri2/core/env.ml
+++ b/src_colibri2/core/env.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/env.mli b/src_colibri2/core/env.mli
index 21da18a3c..192884bec 100644
--- a/src_colibri2/core/env.mli
+++ b/src_colibri2/core/env.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/events.ml b/src_colibri2/core/events.ml
index 0398fdf73..a6d69ec43 100644
--- a/src_colibri2/core/events.ml
+++ b/src_colibri2/core/events.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/events.mli b/src_colibri2/core/events.mli
index a0f82a433..1ea239304 100644
--- a/src_colibri2/core/events.mli
+++ b/src_colibri2/core/events.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/ground.ml b/src_colibri2/core/ground.ml
index 26a9f958e..fb4ca294f 100644
--- a/src_colibri2/core/ground.ml
+++ b/src_colibri2/core/ground.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Nodes
diff --git a/src_colibri2/core/ground.mli b/src_colibri2/core/ground.mli
index 0466e1e3b..d0a830f24 100644
--- a/src_colibri2/core/ground.mli
+++ b/src_colibri2/core/ground.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Nodes
diff --git a/src_colibri2/core/interp.ml b/src_colibri2/core/interp.ml
index eca08223a..ca255f6b8 100644
--- a/src_colibri2/core/interp.ml
+++ b/src_colibri2/core/interp.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/interp.mli b/src_colibri2/core/interp.mli
index ec5491375..3dcfe4ba3 100644
--- a/src_colibri2/core/interp.mli
+++ b/src_colibri2/core/interp.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/domKind.ml b/src_colibri2/core/structures/domKind.ml
index 006a458eb..df4d01380 100644
--- a/src_colibri2/core/structures/domKind.ml
+++ b/src_colibri2/core/structures/domKind.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/domKind.mli b/src_colibri2/core/structures/domKind.mli
index 71cc718a0..2198cf2eb 100644
--- a/src_colibri2/core/structures/domKind.mli
+++ b/src_colibri2/core/structures/domKind.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/expr.ml b/src_colibri2/core/structures/expr.ml
index d8b4c18ce..e2b5c1327 100644
--- a/src_colibri2/core/structures/expr.ml
+++ b/src_colibri2/core/structures/expr.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
include Dolmen_std.Expr
module Ty = struct
diff --git a/src_colibri2/core/structures/nodes.ml b/src_colibri2/core/structures/nodes.ml
index 7c455376f..5e6239f6a 100644
--- a/src_colibri2/core/structures/nodes.ml
+++ b/src_colibri2/core/structures/nodes.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/nodes.mli b/src_colibri2/core/structures/nodes.mli
index 6ab60caa3..200d5181a 100644
--- a/src_colibri2/core/structures/nodes.mli
+++ b/src_colibri2/core/structures/nodes.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/structures/term.ml b/src_colibri2/core/structures/term.ml
index 8755f3615..e3212573b 100644
--- a/src_colibri2/core/structures/term.ml
+++ b/src_colibri2/core/structures/term.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/core/theory.ml b/src_colibri2/core/theory.ml
index add74dd0a..a2ae686a5 100644
--- a/src_colibri2/core/theory.ml
+++ b/src_colibri2/core/theory.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/IArray.ml b/src_colibri2/popop_lib/IArray.ml
index cf071ce33..b81cd0603 100644
--- a/src_colibri2/popop_lib/IArray.ml
+++ b/src_colibri2/popop_lib/IArray.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/IArray.mli b/src_colibri2/popop_lib/IArray.mli
index bb21e7d18..cacc44434 100644
--- a/src_colibri2/popop_lib/IArray.mli
+++ b/src_colibri2/popop_lib/IArray.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/TimeWheel.ml b/src_colibri2/popop_lib/TimeWheel.ml
index 6f606a1aa..66c9667d0 100644
--- a/src_colibri2/popop_lib/TimeWheel.ml
+++ b/src_colibri2/popop_lib/TimeWheel.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Base
(** TimeWheel *)
diff --git a/src_colibri2/popop_lib/TimeWheel.mli b/src_colibri2/popop_lib/TimeWheel.mli
index 1e1583451..47d9fc349 100644
--- a/src_colibri2/popop_lib/TimeWheel.mli
+++ b/src_colibri2/popop_lib/TimeWheel.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** Time Wheel *)
(** Allows to add timestamp in the futur and get the next timestamp.
diff --git a/src_colibri2/popop_lib/enum.ml b/src_colibri2/popop_lib/enum.ml
index 3d7eb0c17..188e08b18 100644
--- a/src_colibri2/popop_lib/enum.ml
+++ b/src_colibri2/popop_lib/enum.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/enum.mli b/src_colibri2/popop_lib/enum.mli
index 01200b460..9abb7a9b7 100644
--- a/src_colibri2/popop_lib/enum.mli
+++ b/src_colibri2/popop_lib/enum.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/popop_stdlib.ml b/src_colibri2/popop_lib/popop_stdlib.ml
index 8d981e9e3..74bfc53b8 100644
--- a/src_colibri2/popop_lib/popop_stdlib.ml
+++ b/src_colibri2/popop_lib/popop_stdlib.ml
@@ -1,22 +1,13 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
module Map = Extmap
module XHashtbl = Exthtbl.Hashtbl
diff --git a/src_colibri2/popop_lib/popop_stdlib.mli b/src_colibri2/popop_lib/popop_stdlib.mli
index 5223769cc..48930dafd 100644
--- a/src_colibri2/popop_lib/popop_stdlib.mli
+++ b/src_colibri2/popop_lib/popop_stdlib.mli
@@ -1,22 +1,13 @@
-(*************************************************************************)
-(* This file is part of Colibrics. *)
-(* *)
-(* Copyright (C) 2017 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(*************************************************************************)
+(********************************************************************)
+(* *)
+(* The Why3 Verification Platform / The Why3 Development Team *)
+(* Copyright 2010-2017 -- INRIA - CNRS - Paris-Sud University *)
+(* *)
+(* This software is distributed under the terms of the GNU Lesser *)
+(* General Public License version 2.1, with the special exception *)
+(* on linking described in file LICENSE. *)
+(* *)
+(********************************************************************)
module Map : module type of Extmap
module XHashtbl : Exthtbl.Hashtbl
diff --git a/src_colibri2/popop_lib/refo.ml b/src_colibri2/popop_lib/refo.ml
index 7fe2a4629..fc8883e62 100644
--- a/src_colibri2/popop_lib/refo.ml
+++ b/src_colibri2/popop_lib/refo.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/refo.mli b/src_colibri2/popop_lib/refo.mli
index a8c8a7076..97b08c18f 100644
--- a/src_colibri2/popop_lib/refo.mli
+++ b/src_colibri2/popop_lib/refo.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/simple_vector.ml b/src_colibri2/popop_lib/simple_vector.ml
index eec41b667..cad47da22 100644
--- a/src_colibri2/popop_lib/simple_vector.ml
+++ b/src_colibri2/popop_lib/simple_vector.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/simple_vector.mli b/src_colibri2/popop_lib/simple_vector.mli
index bb41c8bb0..07d1723af 100644
--- a/src_colibri2/popop_lib/simple_vector.mli
+++ b/src_colibri2/popop_lib/simple_vector.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/unit.ml b/src_colibri2/popop_lib/unit.ml
index d02f635a0..10787b6fe 100644
--- a/src_colibri2/popop_lib/unit.ml
+++ b/src_colibri2/popop_lib/unit.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/unit.mli b/src_colibri2/popop_lib/unit.mli
index 43c11eaeb..330cdac42 100644
--- a/src_colibri2/popop_lib/unit.mli
+++ b/src_colibri2/popop_lib/unit.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/vector_hetero.ml b/src_colibri2/popop_lib/vector_hetero.ml
index e003f2b72..aa991a4d8 100644
--- a/src_colibri2/popop_lib/vector_hetero.ml
+++ b/src_colibri2/popop_lib/vector_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/popop_lib/vector_hetero.mli b/src_colibri2/popop_lib/vector_hetero.mli
index b5d610f42..64705542b 100644
--- a/src_colibri2/popop_lib/vector_hetero.mli
+++ b/src_colibri2/popop_lib/vector_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/input.ml b/src_colibri2/solver/input.ml
index d2533125a..dfd18558f 100644
--- a/src_colibri2/solver/input.ml
+++ b/src_colibri2/solver/input.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/scheduler.ml b/src_colibri2/solver/scheduler.ml
index 267e8528a..ae30079ca 100644
--- a/src_colibri2/solver/scheduler.ml
+++ b/src_colibri2/solver/scheduler.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/scheduler.mli b/src_colibri2/solver/scheduler.mli
index 2bf87eaba..d4c7ee4ea 100644
--- a/src_colibri2/solver/scheduler.mli
+++ b/src_colibri2/solver/scheduler.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/solver/solver.ml b/src_colibri2/solver/solver.ml
index 25c5bee75..c393bb9f8 100644
--- a/src_colibri2/solver/solver.ml
+++ b/src_colibri2/solver/solver.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/comp_keys.ml b/src_colibri2/stdlib/comp_keys.ml
index 1c00173b6..619d2c43d 100644
--- a/src_colibri2/stdlib/comp_keys.ml
+++ b/src_colibri2/stdlib/comp_keys.ml
@@ -1,9 +1,12 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
+(* INRIA (Institut National de Recherche en Informatique et en *)
+(* Automatique) *)
+(* CNRS (Centre national de la recherche scientifique) *)
(* *)
(* you can redistribute it and/or modify it under the terms of the GNU *)
(* Lesser General Public License as published by the Free Software *)
diff --git a/src_colibri2/stdlib/comp_keys.mli b/src_colibri2/stdlib/comp_keys.mli
index 5dc6875c9..b7cf2fca4 100644
--- a/src_colibri2/stdlib/comp_keys.mli
+++ b/src_colibri2/stdlib/comp_keys.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/config.ml b/src_colibri2/stdlib/config.ml
index 4c0c4ea63..0d942b9dd 100644
--- a/src_colibri2/stdlib/config.ml
+++ b/src_colibri2/stdlib/config.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/context.ml b/src_colibri2/stdlib/context.ml
index d890f6f21..a189dcb3e 100644
--- a/src_colibri2/stdlib/context.ml
+++ b/src_colibri2/stdlib/context.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/context.mli b/src_colibri2/stdlib/context.mli
index 8fb3f8b65..bd74832fb 100644
--- a/src_colibri2/stdlib/context.mli
+++ b/src_colibri2/stdlib/context.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero.ml b/src_colibri2/stdlib/hashtbl_hetero.ml
index f83555bf4..ecca80e99 100644
--- a/src_colibri2/stdlib/hashtbl_hetero.ml
+++ b/src_colibri2/stdlib/hashtbl_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero.mli b/src_colibri2/stdlib/hashtbl_hetero.mli
index ee817fff9..fe2f788ad 100644
--- a/src_colibri2/stdlib/hashtbl_hetero.mli
+++ b/src_colibri2/stdlib/hashtbl_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/hashtbl_hetero_sig.ml b/src_colibri2/stdlib/hashtbl_hetero_sig.ml
index 7f32aed63..9aa896b0b 100644
--- a/src_colibri2/stdlib/hashtbl_hetero_sig.ml
+++ b/src_colibri2/stdlib/hashtbl_hetero_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/keys.ml b/src_colibri2/stdlib/keys.ml
index cf4545104..dfc1c0624 100644
--- a/src_colibri2/stdlib/keys.ml
+++ b/src_colibri2/stdlib/keys.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/keys.mli b/src_colibri2/stdlib/keys.mli
index 5d6670ccf..084a1ee91 100644
--- a/src_colibri2/stdlib/keys.mli
+++ b/src_colibri2/stdlib/keys.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/keys_sig.ml b/src_colibri2/stdlib/keys_sig.ml
index 6ae7792bd..8db21311c 100644
--- a/src_colibri2/stdlib/keys_sig.ml
+++ b/src_colibri2/stdlib/keys_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero.ml b/src_colibri2/stdlib/map_hetero.ml
index 1563821d9..306ff33ff 100644
--- a/src_colibri2/stdlib/map_hetero.ml
+++ b/src_colibri2/stdlib/map_hetero.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero.mli b/src_colibri2/stdlib/map_hetero.mli
index 870cdd757..dc1fceb0f 100644
--- a/src_colibri2/stdlib/map_hetero.mli
+++ b/src_colibri2/stdlib/map_hetero.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/map_hetero_sig.ml b/src_colibri2/stdlib/map_hetero_sig.ml
index a6e27e7e0..ada023913 100644
--- a/src_colibri2/stdlib/map_hetero_sig.ml
+++ b/src_colibri2/stdlib/map_hetero_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/shuffle.ml b/src_colibri2/stdlib/shuffle.ml
index 8d127a417..4001bd632 100644
--- a/src_colibri2/stdlib/shuffle.ml
+++ b/src_colibri2/stdlib/shuffle.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/shuffle.mli b/src_colibri2/stdlib/shuffle.mli
index e014b4180..15f48f2b1 100644
--- a/src_colibri2/stdlib/shuffle.mli
+++ b/src_colibri2/stdlib/shuffle.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/std.ml b/src_colibri2/stdlib/std.ml
index c9f8302dc..f3764175d 100644
--- a/src_colibri2/stdlib/std.ml
+++ b/src_colibri2/stdlib/std.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/std.mli b/src_colibri2/stdlib/std.mli
index 8433dd5b7..625d917cd 100644
--- a/src_colibri2/stdlib/std.mli
+++ b/src_colibri2/stdlib/std.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibri2. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2017-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* INRIA (Institut National de Recherche en Informatique et en *)
diff --git a/src_colibri2/stdlib/std_sig.ml b/src_colibri2/stdlib/std_sig.ml
index 42862b932..5c73e0f56 100644
--- a/src_colibri2/stdlib/std_sig.ml
+++ b/src_colibri2/stdlib/std_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/stdlib/wto.ml b/src_colibri2/stdlib/wto.ml
index f7a4d3d58..09fa2038d 100644
--- a/src_colibri2/stdlib/wto.ml
+++ b/src_colibri2/stdlib/wto.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
(** Each component of the graph is either an individual node of the graph
(without) self loop, or a strongly connected component where a node is
diff --git a/src_colibri2/stdlib/wto.mli b/src_colibri2/stdlib/wto.mli
index a4226b3b9..d3e6ad31f 100644
--- a/src_colibri2/stdlib/wto.mli
+++ b/src_colibri2/stdlib/wto.mli
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
(** Weak topological orderings (WTOs) are a hierarchical decomposition of the
a graph where each layer is topologically ordered and strongly connected
diff --git a/src_colibri2/tests/generate_tests/generate_dune_tests.ml b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
index 0c8480878..7094b142d 100644
--- a/src_colibri2/tests/generate_tests/generate_dune_tests.ml
+++ b/src_colibri2/tests/generate_tests/generate_dune_tests.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
let dir = Sys.argv.(1)
let result = Sys.argv.(2)
diff --git a/src_colibri2/tests/test.ml b/src_colibri2/tests/test.ml
index 5d8d12caa..216770b53 100644
--- a/src_colibri2/tests/test.ml
+++ b/src_colibri2/tests/test.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests.ml b/src_colibri2/tests/tests.ml
index ef4d208e1..63215c388 100644
--- a/src_colibri2/tests/tests.ml
+++ b/src_colibri2/tests/tests.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_LRA.ml b/src_colibri2/tests/tests_LRA.ml
index 0f2074808..16087451d 100644
--- a/src_colibri2/tests/tests_LRA.ml
+++ b/src_colibri2/tests/tests_LRA.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_bool.ml b/src_colibri2/tests/tests_bool.ml
index 07cdfb4e1..6be56a2d5 100644
--- a/src_colibri2/tests/tests_bool.ml
+++ b/src_colibri2/tests/tests_bool.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_lib.ml b/src_colibri2/tests/tests_lib.ml
index 54d7784e0..25c9d95bf 100644
--- a/src_colibri2/tests/tests_lib.ml
+++ b/src_colibri2/tests/tests_lib.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/tests/tests_uf.ml b/src_colibri2/tests/tests_uf.ml
index af42f372e..c694356f3 100644
--- a/src_colibri2/tests/tests_uf.ml
+++ b/src_colibri2/tests/tests_uf.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/ADT/adt.ml b/src_colibri2/theories/ADT/adt.ml
index e8b62ee40..8f4925404 100644
--- a/src_colibri2/theories/ADT/adt.ml
+++ b/src_colibri2/theories/ADT/adt.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Colibri2_popop_lib.Popop_stdlib
module Case = DInt
diff --git a/src_colibri2/theories/ADT/adt.mli b/src_colibri2/theories/ADT/adt.mli
index 091896da1..f7e23aa70 100644
--- a/src_colibri2/theories/ADT/adt.mli
+++ b/src_colibri2/theories/ADT/adt.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
val init : Egraph.t -> unit
diff --git a/src_colibri2/theories/ADT/adt_value.ml b/src_colibri2/theories/ADT/adt_value.ml
index eb1c0974e..eb7b4f9e3 100644
--- a/src_colibri2/theories/ADT/adt_value.ml
+++ b/src_colibri2/theories/ADT/adt_value.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Base
open Colibri2_core
open Colibri2_popop_lib.Popop_stdlib
diff --git a/src_colibri2/theories/ADT/adt_value.mli b/src_colibri2/theories/ADT/adt_value.mli
index 7ebbb8b70..65b7b6374 100644
--- a/src_colibri2/theories/ADT/adt_value.mli
+++ b/src_colibri2/theories/ADT/adt_value.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib.Popop_stdlib
module Case = DInt
module Field = DInt
diff --git a/src_colibri2/theories/LRA/LRA.ml b/src_colibri2/theories/LRA/LRA.ml
index 3065286b5..b9f35ca93 100644
--- a/src_colibri2/theories/LRA/LRA.ml
+++ b/src_colibri2/theories/LRA/LRA.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/LRA.mli b/src_colibri2/theories/LRA/LRA.mli
index 47b7125b4..040771d54 100644
--- a/src_colibri2/theories/LRA/LRA.mli
+++ b/src_colibri2/theories/LRA/LRA.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/delta.ml b/src_colibri2/theories/LRA/delta.ml
index c5e9c5649..dc3448d58 100644
--- a/src_colibri2/theories/LRA/delta.ml
+++ b/src_colibri2/theories/LRA/delta.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** Currently the distance graph only store information and reacts to change, it
doesn't compute distances *)
diff --git a/src_colibri2/theories/LRA/delta.mli b/src_colibri2/theories/LRA/delta.mli
index 3724460a6..ff733676e 100644
--- a/src_colibri2/theories/LRA/delta.mli
+++ b/src_colibri2/theories/LRA/delta.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** Distance Graph *)
diff --git a/src_colibri2/theories/LRA/dom_interval.ml b/src_colibri2/theories/LRA/dom_interval.ml
index b362031ac..863fd7a35 100644
--- a/src_colibri2/theories/LRA/dom_interval.ml
+++ b/src_colibri2/theories/LRA/dom_interval.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_interval.mli b/src_colibri2/theories/LRA/dom_interval.mli
index 3a4919feb..d610137c3 100644
--- a/src_colibri2/theories/LRA/dom_interval.mli
+++ b/src_colibri2/theories/LRA/dom_interval.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
module D: sig type t end
diff --git a/src_colibri2/theories/LRA/dom_polynome.ml b/src_colibri2/theories/LRA/dom_polynome.ml
index 55052ceef..a1ad365b6 100644
--- a/src_colibri2/theories/LRA/dom_polynome.ml
+++ b/src_colibri2/theories/LRA/dom_polynome.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_polynome.mli b/src_colibri2/theories/LRA/dom_polynome.mli
index 4c3518172..1b28c48f4 100644
--- a/src_colibri2/theories/LRA/dom_polynome.mli
+++ b/src_colibri2/theories/LRA/dom_polynome.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_product.ml b/src_colibri2/theories/LRA/dom_product.ml
index 5907e5f0e..e0d5b4280 100644
--- a/src_colibri2/theories/LRA/dom_product.ml
+++ b/src_colibri2/theories/LRA/dom_product.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/dom_product.mli b/src_colibri2/theories/LRA/dom_product.mli
index 79b40b11e..06de5f286 100644
--- a/src_colibri2/theories/LRA/dom_product.mli
+++ b/src_colibri2/theories/LRA/dom_product.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/fourier.ml b/src_colibri2/theories/LRA/fourier.ml
index f6e378549..118bcebca 100644
--- a/src_colibri2/theories/LRA/fourier.ml
+++ b/src_colibri2/theories/LRA/fourier.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Colibri2_core
diff --git a/src_colibri2/theories/LRA/fourier.mli b/src_colibri2/theories/LRA/fourier.mli
index d8be888cc..13235f23e 100644
--- a/src_colibri2/theories/LRA/fourier.mli
+++ b/src_colibri2/theories/LRA/fourier.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.ml b/src_colibri2/theories/LRA/integer_sign_domain.ml
index e521eea13..69981140f 100644
--- a/src_colibri2/theories/LRA/integer_sign_domain.ml
+++ b/src_colibri2/theories/LRA/integer_sign_domain.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
(** Sign domain with integer. *)
diff --git a/src_colibri2/theories/LRA/integer_sign_domain.mli b/src_colibri2/theories/LRA/integer_sign_domain.mli
index c2dec4a2d..265e418b6 100644
--- a/src_colibri2/theories/LRA/integer_sign_domain.mli
+++ b/src_colibri2/theories/LRA/integer_sign_domain.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
include Interval_sig.S
type split_heuristic =
diff --git a/src_colibri2/theories/LRA/interval.ml b/src_colibri2/theories/LRA/interval.ml
index 1086386e9..e18159736 100644
--- a/src_colibri2/theories/LRA/interval.ml
+++ b/src_colibri2/theories/LRA/interval.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/interval.mli b/src_colibri2/theories/LRA/interval.mli
index 92d6acbc9..6625bb4ce 100644
--- a/src_colibri2/theories/LRA/interval.mli
+++ b/src_colibri2/theories/LRA/interval.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/interval_sig.ml b/src_colibri2/theories/LRA/interval_sig.ml
index 741b47a96..b318a09f2 100644
--- a/src_colibri2/theories/LRA/interval_sig.ml
+++ b/src_colibri2/theories/LRA/interval_sig.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/mul.ml b/src_colibri2/theories/LRA/mul.ml
index 50d80ce35..1cdfdc52d 100644
--- a/src_colibri2/theories/LRA/mul.ml
+++ b/src_colibri2/theories/LRA/mul.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
let init,attach =
Demon.Fast.register_get_value_daemon
~name:"Mul.get_value"
diff --git a/src_colibri2/theories/LRA/mul.mli b/src_colibri2/theories/LRA/mul.mli
index d8be888cc..13235f23e 100644
--- a/src_colibri2/theories/LRA/mul.mli
+++ b/src_colibri2/theories/LRA/mul.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
val init: Egraph.t -> unit
diff --git a/src_colibri2/theories/LRA/polynome.ml b/src_colibri2/theories/LRA/polynome.ml
index 8a7900a48..fcec24d72 100644
--- a/src_colibri2/theories/LRA/polynome.ml
+++ b/src_colibri2/theories/LRA/polynome.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/polynome.mli b/src_colibri2/theories/LRA/polynome.mli
index bd9ada2d3..48ac39203 100644
--- a/src_colibri2/theories/LRA/polynome.mli
+++ b/src_colibri2/theories/LRA/polynome.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/product.ml b/src_colibri2/theories/LRA/product.ml
index 40da25d94..c971e576b 100644
--- a/src_colibri2/theories/LRA/product.ml
+++ b/src_colibri2/theories/LRA/product.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/product.mli b/src_colibri2/theories/LRA/product.mli
index ae36c7654..dfca11762 100644
--- a/src_colibri2/theories/LRA/product.mli
+++ b/src_colibri2/theories/LRA/product.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/realValue.ml b/src_colibri2/theories/LRA/realValue.ml
index 4410b095a..4cb58a994 100644
--- a/src_colibri2/theories/LRA/realValue.ml
+++ b/src_colibri2/theories/LRA/realValue.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/realValue.mli b/src_colibri2/theories/LRA/realValue.mli
index 00551a1e1..4bfd3fa33 100644
--- a/src_colibri2/theories/LRA/realValue.mli
+++ b/src_colibri2/theories/LRA/realValue.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/LRA/sign_domain.ml b/src_colibri2/theories/LRA/sign_domain.ml
index 5d4cb69a8..a4df04b23 100644
--- a/src_colibri2/theories/LRA/sign_domain.ml
+++ b/src_colibri2/theories/LRA/sign_domain.ml
@@ -1,24 +1,22 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2020 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
(** Sign domain: abstraction of integer numerical values by their signs. *)
(** From frama-c *)
diff --git a/src_colibri2/theories/LRA/sign_domain.mli b/src_colibri2/theories/LRA/sign_domain.mli
index 65ed7df7e..f8a18f2a9 100644
--- a/src_colibri2/theories/LRA/sign_domain.mli
+++ b/src_colibri2/theories/LRA/sign_domain.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t = private {
pos: bool;
zero: bool;
diff --git a/src_colibri2/theories/bool/boolean.ml b/src_colibri2/theories/bool/boolean.ml
index 7b8ce5a30..77e415502 100644
--- a/src_colibri2/theories/bool/boolean.ml
+++ b/src_colibri2/theories/bool/boolean.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/boolean.mli b/src_colibri2/theories/bool/boolean.mli
index c170d909a..b44c27b84 100644
--- a/src_colibri2/theories/bool/boolean.mli
+++ b/src_colibri2/theories/bool/boolean.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/equality.ml b/src_colibri2/theories/bool/equality.ml
index b0234ea78..e30cfc12b 100644
--- a/src_colibri2/theories/bool/equality.ml
+++ b/src_colibri2/theories/bool/equality.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/bool/equality.mli b/src_colibri2/theories/bool/equality.mli
index 9cabfdec5..c9cbc7b0f 100644
--- a/src_colibri2/theories/bool/equality.mli
+++ b/src_colibri2/theories/bool/equality.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/quantifier/F.ml b/src_colibri2/theories/quantifier/F.ml
index 5808c457a..6f94c1d7d 100644
--- a/src_colibri2/theories/quantifier/F.ml
+++ b/src_colibri2/theories/quantifier/F.ml
@@ -1,2 +1,22 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
include Expr.Term.Const
module EnvApps = Datastructure.Memo (Expr.Term.Const)
diff --git a/src_colibri2/theories/quantifier/FA.ml b/src_colibri2/theories/quantifier/FA.ml
index 3e0c8f761..513ee4dd5 100644
--- a/src_colibri2/theories/quantifier/FA.ml
+++ b/src_colibri2/theories/quantifier/FA.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** instantiated function symbol *)
module T = struct
let hash_fold_list = Base.hash_fold_list
diff --git a/src_colibri2/theories/quantifier/F_Pos.ml b/src_colibri2/theories/quantifier/F_Pos.ml
index 129677c36..8b6d370fa 100644
--- a/src_colibri2/theories/quantifier/F_Pos.ml
+++ b/src_colibri2/theories/quantifier/F_Pos.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** A position inside a function symbol *)
diff --git a/src_colibri2/theories/quantifier/F_Pos.mli b/src_colibri2/theories/quantifier/F_Pos.mli
index 147e5028a..eb5281b9b 100644
--- a/src_colibri2/theories/quantifier/F_Pos.mli
+++ b/src_colibri2/theories/quantifier/F_Pos.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** A position inside a function symbol *)
type t = { f : F.t; pos : int }
diff --git a/src_colibri2/theories/quantifier/InvertedPath.ml b/src_colibri2/theories/quantifier/InvertedPath.ml
index 7cfbd188b..3949f6175 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.ml
+++ b/src_colibri2/theories/quantifier/InvertedPath.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/InvertedPath.mli b/src_colibri2/theories/quantifier/InvertedPath.mli
index 9c0eda7e9..c2a1ed3b0 100644
--- a/src_colibri2/theories/quantifier/InvertedPath.mli
+++ b/src_colibri2/theories/quantifier/InvertedPath.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t
(** An InvertedPath is a way to go from one subterm of patterns to substitution
of triggers. It allows to know which nodes merge can create new substitutions
diff --git a/src_colibri2/theories/quantifier/PC.ml b/src_colibri2/theories/quantifier/PC.ml
index 76c828be0..beb25bb73 100644
--- a/src_colibri2/theories/quantifier/PC.ml
+++ b/src_colibri2/theories/quantifier/PC.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PC.mli b/src_colibri2/theories/quantifier/PC.mli
index f6c39f6f0..aea6513be 100644
--- a/src_colibri2/theories/quantifier/PC.mli
+++ b/src_colibri2/theories/quantifier/PC.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t = { parent : F_Pos.t; child : F.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/PN.ml b/src_colibri2/theories/quantifier/PN.ml
index 608538eee..5990eb675 100644
--- a/src_colibri2/theories/quantifier/PN.ml
+++ b/src_colibri2/theories/quantifier/PN.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PN.mli b/src_colibri2/theories/quantifier/PN.mli
index d3a676cbf..48104c257 100644
--- a/src_colibri2/theories/quantifier/PN.mli
+++ b/src_colibri2/theories/quantifier/PN.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t = { parent : F_Pos.t; node : Node.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/PP.ml b/src_colibri2/theories/quantifier/PP.ml
index 903815458..4a664df57 100644
--- a/src_colibri2/theories/quantifier/PP.ml
+++ b/src_colibri2/theories/quantifier/PP.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
module T = struct
diff --git a/src_colibri2/theories/quantifier/PP.mli b/src_colibri2/theories/quantifier/PP.mli
index 3302a3c13..64acb2a2e 100644
--- a/src_colibri2/theories/quantifier/PP.mli
+++ b/src_colibri2/theories/quantifier/PP.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t = private { parent1 : F_Pos.t; parent2 : F_Pos.t }
include Colibri2_popop_lib.Popop_stdlib.Datatype with type t := t
diff --git a/src_colibri2/theories/quantifier/common.ml b/src_colibri2/theories/quantifier/common.ml
index 694237dad..21405040c 100644
--- a/src_colibri2/theories/quantifier/common.ml
+++ b/src_colibri2/theories/quantifier/common.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
let debug =
diff --git a/src_colibri2/theories/quantifier/info.ml b/src_colibri2/theories/quantifier/info.ml
index df42bb012..632f809a7 100644
--- a/src_colibri2/theories/quantifier/info.ml
+++ b/src_colibri2/theories/quantifier/info.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** information added on nodes *)
diff --git a/src_colibri2/theories/quantifier/info.mli b/src_colibri2/theories/quantifier/info.mli
index 2b8dc0171..700c2c538 100644
--- a/src_colibri2/theories/quantifier/info.mli
+++ b/src_colibri2/theories/quantifier/info.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
type t = {
parents : Ground.S.t F_Pos.M.t; (** parents *)
apps : Ground.S.t F.M.t; (** parent parent *)
diff --git a/src_colibri2/theories/quantifier/pattern.ml b/src_colibri2/theories/quantifier/pattern.ml
index 3412d3f4e..3128b8e30 100644
--- a/src_colibri2/theories/quantifier/pattern.ml
+++ b/src_colibri2/theories/quantifier/pattern.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/pattern.mli b/src_colibri2/theories/quantifier/pattern.mli
index b820c35f9..235ef0f22 100644
--- a/src_colibri2/theories/quantifier/pattern.mli
+++ b/src_colibri2/theories/quantifier/pattern.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
(** Pattern *)
diff --git a/src_colibri2/theories/quantifier/quantifier.ml b/src_colibri2/theories/quantifier/quantifier.ml
index aff0944fd..6f9e1f57f 100644
--- a/src_colibri2/theories/quantifier/quantifier.ml
+++ b/src_colibri2/theories/quantifier/quantifier.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** Cf Efficient E-Matching paper *)
open Colibri2_popop_lib
diff --git a/src_colibri2/theories/quantifier/quantifier.mli b/src_colibri2/theories/quantifier/quantifier.mli
index 884026c74..164992ff9 100644
--- a/src_colibri2/theories/quantifier/quantifier.mli
+++ b/src_colibri2/theories/quantifier/quantifier.mli
@@ -1 +1,21 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
val th_register : Egraph.t -> unit
diff --git a/src_colibri2/theories/quantifier/trigger.ml b/src_colibri2/theories/quantifier/trigger.ml
index d8f35bb6f..c4c447bfe 100644
--- a/src_colibri2/theories/quantifier/trigger.ml
+++ b/src_colibri2/theories/quantifier/trigger.ml
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
open Colibri2_popop_lib
open Common
diff --git a/src_colibri2/theories/quantifier/trigger.mli b/src_colibri2/theories/quantifier/trigger.mli
index f1cffad60..8dca75064 100644
--- a/src_colibri2/theories/quantifier/trigger.mli
+++ b/src_colibri2/theories/quantifier/trigger.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
(** Trigger *)
type t = {
diff --git a/src_colibri2/theories/quantifier/uninterp.ml b/src_colibri2/theories/quantifier/uninterp.ml
index a20932dd6..a4e4615ac 100644
--- a/src_colibri2/theories/quantifier/uninterp.ml
+++ b/src_colibri2/theories/quantifier/uninterp.ml
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
diff --git a/src_colibri2/theories/quantifier/uninterp.mli b/src_colibri2/theories/quantifier/uninterp.mli
index 952f5027f..f3a829594 100644
--- a/src_colibri2/theories/quantifier/uninterp.mli
+++ b/src_colibri2/theories/quantifier/uninterp.mli
@@ -1,7 +1,7 @@
(*************************************************************************)
-(* This file is part of Colibrics. *)
+(* This file is part of Colibri2. *)
(* *)
-(* Copyright (C) 2017 *)
+(* Copyright (C) 2014-2021 *)
(* CEA (Commissariat à l'énergie atomique et aux énergies *)
(* alternatives) *)
(* *)
--
GitLab