aboutsummaryrefslogtreecommitdiffstats
path: root/src/trace
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/trace
parent3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (diff)
downloadsmtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.tar.gz
smtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.zip
Updating of the copyright
Diffstat (limited to 'src/trace')
-rw-r--r--src/trace/coqTerms.ml5
-rw-r--r--src/trace/satAtom.ml5
-rw-r--r--src/trace/smtAtom.ml5
-rw-r--r--src/trace/smtAtom.mli4
-rw-r--r--src/trace/smtCertif.ml4
-rw-r--r--src/trace/smtCnf.ml4
-rw-r--r--src/trace/smtCommands.ml16
-rw-r--r--src/trace/smtForm.ml6
-rw-r--r--src/trace/smtForm.mli5
-rw-r--r--src/trace/smtMisc.ml4
-rw-r--r--src/trace/smtTrace.ml6
-rw-r--r--src/trace/smt_tactic.ml44
12 files changed, 46 insertions, 22 deletions
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 429ed72..d405894 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.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 *)
(* *)
(**************************************************************************)
+
open Coqlib
let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index f381407..f65e850 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.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 *)
(* *)
(**************************************************************************)
+
open SmtMisc
open CoqTerms
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 979e4e4..832778a 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.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 *)
(* *)
(**************************************************************************)
+
open SmtMisc
open CoqTerms
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index fd0a30c..cdcdcd1 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 76036a5..6a56c43 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
diff --git a/src/trace/smtCnf.ml b/src/trace/smtCnf.ml
index f2a06c8..bf3d0d1 100644
--- a/src/trace/smtCnf.ml
+++ b/src/trace/smtCnf.ml
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index b019f24..bace2d2 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -1,3 +1,19 @@
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Michaël Armand *)
+(* Benjamin Grégoire *)
+(* Chantal Keller *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
+
open Entries
open Declare
open Decl_kinds
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 7dc727a..8f2fea8 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -1,17 +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 *)
(* *)
(**************************************************************************)
+
+
open Util
open SmtMisc
open CoqTerms
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index 118ecf5..2a00228 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -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 *)
(* *)
(**************************************************************************)
+
module type ATOM =
sig
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 21d81dc..1ad92ac 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b96807f..e2a9b1d 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -1,17 +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 *)
(* *)
(**************************************************************************)
+
+
open SmtMisc
open CoqTerms
open SmtCertif
diff --git a/src/trace/smt_tactic.ml4 b/src/trace/smt_tactic.ml4
index a1f8790..d3fca95 100644
--- a/src/trace/smt_tactic.ml4
+++ b/src/trace/smt_tactic.ml4
@@ -1,13 +1,13 @@
(**************************************************************************)
(* *)
(* 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 *)
(* *)
generated by cgit (git 2.34.1) at 2024-06-29 02:56:34 +0000