aboutsummaryrefslogtreecommitdiffstats
path: root/src/lia
diff options
context:
space:
mode:
authorChantal Keller <Chantal.Keller@lri.fr>2016-04-27 00:17:33 +0200
committerChantal Keller <Chantal.Keller@lri.fr>2016-04-27 00:17:33 +0200
commitd734e4eae47b0b7f13626053663d236faa7f69e6 (patch)
tree52667d0b8931ccb73e132c2bf13772f51187f9c3 /src/lia
parent3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (diff)
downloadsmtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.tar.gz
smtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.zip
Updating of the copyright
Diffstat (limited to 'src/lia')
-rw-r--r--src/lia/Lia.v5
-rw-r--r--src/lia/lia.ml5
2 files changed, 6 insertions, 4 deletions
diff --git a/src/lia/Lia.v b/src/lia/Lia.v
index 13a2405..977612f 100644
--- a/src/lia/Lia.v
+++ b/src/lia/Lia.v
@@ -1,18 +1,19 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
-(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
+
Require Import Bool.
Require Import List.
Require Import Int63.
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 97415b9..de291da 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -1,18 +1,19 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Michaël Armand *)
(* Benjamin Grégoire *)
(* Chantal Keller *)
(* *)
-(* Inria - École Polytechnique - MSR-Inria Joint Lab *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
(* *)
(* This file is distributed under the terms of the CeCILL-C licence *)
(* *)
(**************************************************************************)
+
(*** Linking SMT Terms to Micromega Terms ***)
open Term
open Coqlib