Skip to content

Commit

Permalink
Change license from CeCILL v2 to MPL-2.0 (more permissive) (#208)
Browse files Browse the repository at this point in the history 
* relicense to MPL-2.0 using a script

* changing license field in opam file, thx to @Zimmi48

* renamed MPL-2.0 license file for GitHub automatic recognition
  • Loading branch information
@DmxLarchey @yforster
DmxLarchey authored and yforster committed Nov 2, 2023
1 parent a36e9ab commit 8880e19
Show file tree
Hide file tree
Showing 215 changed files with 586 additions and 732 deletions.
519 changes: 0 additions & 519 deletions CeCILL_LICENSE.txt
View file

This file was deleted.

373 changes: 373 additions & 0 deletions LICENSE
View file

Large diffs are not rendered by default.

2 changes: 1 addition & 1 deletion opam
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@ authors: ["Yannick Forster"
"Dominik Wehr"
"Maxi Wuttke"]

license: "CECILL-2.1"
license: "MPL-2.0"
build: [
[make "-j%{jobs}%"]
]
Expand Down
2 changes: 1 addition & 1 deletion theories/DiophantineConstraints/Reductions/FRACTRAN_to_H10C_SAT.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Max.
Expand Down
2 changes: 1 addition & 1 deletion theories/DiophantineConstraints/Util/h10c_utils.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

(* Elementary Diophantine constraints w/o parameters
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/BPCP_SigBPCP.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(* [+] Affiliation U. Sarrbrucken *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

(* This was implemented by DLW following the ideas of
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig0.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Max.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig1.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig1_1.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig2_SigSSn1.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig2_Sign.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_Sig_fin.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec Max.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_discernable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Bool.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_discrete.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_no_syms.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_noeq.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Relations.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_one_rel.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

(* The code was initially developed by Dominik Kirst to be
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_rem_constants.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_rem_cst.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_rem_props.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_rem_syms.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sig_uniform.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sign1_Sig.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sign_Sig.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/Sign_Sig2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/bpcp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Bool.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/btree.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

(* This file is mainly a complete re-implementation of the
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/decidable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/discernable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Bool.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/discrete.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Nat Lia Relations Bool.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/enumerable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_congruence.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Relations.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_definable.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_enum.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Max.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_logic.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_sat.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_sat_dec.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_sig.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fo_terms.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/fol_ops.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/gfp.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Nat Lia Relations.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/hfs.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Lia Max Wellfounded Setoid Eqdep_dec Bool.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/membership.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Nat Lia Max Wellfounded Coq.Setoids.Setoid.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/notations.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/red_chain_undec_full.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith Bool Lia Eqdep_dec.
Expand Down
2 changes: 1 addition & 1 deletion theories/FOL/TRAKHTENBROT/red_dec.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
(* [*] Affiliation LORIA -- CNRS *)
(**************************************************************)
(* This file is distributed under the terms of the *)
(* CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT *)
(* Mozilla Public License Version 2.0, MPL-2.0 *)
(**************************************************************)

Require Import List Arith.
Expand Down
Loading

0 comments on commit 8880e19

Please sign in to comment.