Skip to content

Commit

Permalink
Use separated headers (OCamlPro#1142)
Browse files Browse the repository at this point in the history 
Use separated headers to distinguish our recent contributions and remove years' mentions in copyright as it is not 
a legal mandatory.
  • Loading branch information
@Halbaroth
Halbaroth authored Jul 30, 2024
1 parent 518dcc8 commit f7796d1
Show file tree
Hide file tree
Showing 196 changed files with 223 additions and 433 deletions.
2 changes: 1 addition & 1 deletion examples/lib_usage.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion licenses/free-header.txt
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

Alt-Ergo: The SMT Solver For Software Verification
Copyright (C) 2013-2024 --- OCamlPro SAS
Copyright (C) --- OCamlPro SAS

This is an exceptional free release of Alt-Ergo dual-licensed
under the OCamlPro-Non-Commercial-License and
Expand Down
11 changes: 1 addition & 10 deletions licenses/header.txt
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@

Alt-Ergo: The SMT Solver For Software Verification
Copyright (C) 2013-2024 --- OCamlPro SAS
Copyright (C) --- OCamlPro SAS

This file is distributed under the terms of OCamlPro
Non-Commercial Purpose License, version 1.
Expand All @@ -11,14 +11,5 @@

---------------------------------------------------------------

The Alt-Ergo theorem prover

Sylvain Conchon, Evelyne Contejean, Francois Bobot
Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout

CNRS - INRIA - Universite Paris Sud

---------------------------------------------------------------

More details can be found in the directory licenses/

24 changes: 24 additions & 0 deletions licenses/old-header.txt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@

Alt-Ergo: The SMT Solver For Software Verification
Copyright (C) --- OCamlPro SAS

This file is distributed under the terms of OCamlPro
Non-Commercial Purpose License, version 1.

As an exception, Alt-Ergo Club members at the Gold level can
use this file under the terms of the Apache Software License
version 2.0.

---------------------------------------------------------------

The Alt-Ergo theorem prover

Sylvain Conchon, Evelyne Contejean, Francois Bobot
Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout

CNRS - INRIA - Universite Paris Sud

---------------------------------------------------------------

More details can be found in the directory licenses/

10 changes: 5 additions & 5 deletions rsc/extra/headers/alt-ergo_header_ocamlpro.txt
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
Alt-Ergo: The SMT Solver For Software Verification
Copyright (C) 2013-2017 --- OCamlPro SAS

Alt-Ergo: The SMT Solver For Software Verification
Copyright (C) 2013-2017 --- OCamlPro SAS

This file is distributed under the terms of the license indicated
in the file 'License.OCamlPro'. If 'License.OCamlPro' is not
present, please contact us to clarify licensing.

2 changes: 1 addition & 1 deletion rsc/extra/ocamldot/ocamldot.mll
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion rsc/extra/ocpchecker/ocp_checker.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/config.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/input_frontend.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/input_frontend.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/myDynlink.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/myDynlink.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/parse_command.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/parse_command.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/signals_profiling.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/signals_profiling.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/solving_loop.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/common/solving_loop.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/main_text_js.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/options_interface.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/options_interface.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/worker_example.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/worker_interface.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/worker_interface.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/js/worker_js.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/text/main_text.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/bin/text/main_text.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/lib/frontend/cnf.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
2 changes: 1 addition & 1 deletion src/lib/frontend/cnf.mli
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand Down
11 changes: 1 addition & 10 deletions src/lib/frontend/d_cnf.ml
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(**************************************************************************)
(* *)
(* Alt-Ergo: The SMT Solver For Software Verification *)
(* Copyright (C) 2013-2024 --- OCamlPro SAS *)
(* Copyright (C) --- OCamlPro SAS *)
(* *)
(* This file is distributed under the terms of OCamlPro *)
(* Non-Commercial Purpose License, version 1. *)
Expand All @@ -12,15 +12,6 @@
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* The Alt-Ergo theorem prover *)
(* *)
(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *)
(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *)
(* *)
(* CNRS - INRIA - Universite Paris Sud *)
(* *)
(* --------------------------------------------------------------- *)
(* *)
(* More details can be found in the directory licenses/ *)
(* *)
(**************************************************************************)
Expand Down
Loading

0 comments on commit f7796d1

Please sign in to comment.