From d734e4eae47b0b7f13626053663d236faa7f69e6 Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Wed, 27 Apr 2016 00:17:33 +0200 Subject: Updating of the copyright --- src/trace/coqTerms.ml | 5 +++-- src/trace/satAtom.ml | 5 +++-- src/trace/smtAtom.ml | 5 +++-- src/trace/smtAtom.mli | 4 ++-- src/trace/smtCertif.ml | 4 ++-- src/trace/smtCnf.ml | 4 ++-- src/trace/smtCommands.ml | 16 ++++++++++++++++ src/trace/smtForm.ml | 6 ++++-- src/trace/smtForm.mli | 5 +++-- src/trace/smtMisc.ml | 4 ++-- src/trace/smtTrace.ml | 6 ++++-- src/trace/smt_tactic.ml4 | 4 ++-- 12 files changed, 46 insertions(+), 22 deletions(-) (limited to 'src/trace') 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 *) (* *) -- cgit