aboutsummaryrefslogtreecommitdiffstats
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
parent3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (diff)
downloadsmtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.tar.gz
smtcoq-d734e4eae47b0b7f13626053663d236faa7f69e6.zip
Updating of the copyright
-rw-r--r--src/Misc.v4
-rw-r--r--src/SMTCoq.v4
-rw-r--r--src/SMT_terms.v4
-rw-r--r--src/State.v4
-rw-r--r--src/Trace.v4
-rw-r--r--src/cnf/Cnf.v5
-rw-r--r--src/euf/Euf.v6
-rw-r--r--src/extraction/Extract.v4
-rw-r--r--src/extraction/extrNative.ml16
-rw-r--r--src/extraction/extrNative.mli16
-rw-r--r--src/extraction/sat_checker.ml16
-rw-r--r--src/extraction/sat_checker.mli16
-rw-r--r--src/extraction/smt_checker.ml16
-rw-r--r--src/extraction/smt_checker.mli16
-rw-r--r--src/extraction/smtcoq.ml16
-rw-r--r--src/extraction/test.ml16
-rw-r--r--src/extraction/verit_checker.ml16
-rw-r--r--src/extraction/zchaff_checker.ml16
-rw-r--r--src/lia/Lia.v5
-rw-r--r--src/lia/lia.ml5
-rw-r--r--src/smtlib2/smtlib2_genConstr.ml5
-rw-r--r--src/spl/Arithmetic.v5
-rw-r--r--src/spl/Operators.v5
-rw-r--r--src/spl/Syntactic.v5
-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
-rw-r--r--src/verit/verit.ml4
-rw-r--r--src/verit/veritLexer.mll5
-rw-r--r--src/verit/veritParser.mly5
-rw-r--r--src/verit/veritSyntax.ml4
-rw-r--r--src/verit/veritSyntax.mli5
-rw-r--r--src/versions/native/structures.ml4
-rw-r--r--src/versions/standard/Array/PArray_standard.v6
-rw-r--r--src/versions/standard/Int63/Cyclic63_standard.v29
-rw-r--r--src/versions/standard/Int63/Int63Axioms_standard.v10
-rw-r--r--src/versions/standard/Int63/Int63Lib_standard.v27
-rw-r--r--src/versions/standard/Int63/Int63Native_standard.v10
-rw-r--r--src/versions/standard/Int63/Int63Op_standard.v10
-rw-r--r--src/versions/standard/Int63/Int63Properties_standard.v10
-rw-r--r--src/versions/standard/Int63/Int63_standard.v10
-rw-r--r--src/versions/standard/Int63/Ring63_standard.v25
-rw-r--r--src/versions/standard/structures.ml4
-rw-r--r--src/zchaff/cnfParser.ml5
-rw-r--r--src/zchaff/satParser.ml5
-rw-r--r--src/zchaff/zchaff.ml4
-rw-r--r--src/zchaff/zchaffParser.ml6
56 files changed, 359 insertions, 122 deletions
diff --git a/src/Misc.v b/src/Misc.v
index 223c3b6..a7ba19d 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -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/SMTCoq.v b/src/SMTCoq.v
index 54c18e3..40ef316 100644
--- a/src/SMTCoq.v
+++ b/src/SMTCoq.v
@@ -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/SMT_terms.v b/src/SMT_terms.v
index daca0f2..a99c158 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -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/State.v b/src/State.v
index 0830ac6..fde25f9 100644
--- a/src/State.v
+++ b/src/State.v
@@ -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.v b/src/Trace.v
index a7069c1..9ae42c2 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -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/cnf/Cnf.v b/src/cnf/Cnf.v
index fb70223..b5ecfb0 100644
--- a/src/cnf/Cnf.v
+++ b/src/cnf/Cnf.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 *)
(* *)
(**************************************************************************)
+
(* Add LoadPath ".." as SMTCoq. *)
Require Import PArray List Bool.
Require Import Misc State SMT_terms.
diff --git a/src/euf/Euf.v b/src/euf/Euf.v
index e3d73f6..53e3ebe 100644
--- a/src/euf/Euf.v
+++ b/src/euf/Euf.v
@@ -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 *)
(* *)
(**************************************************************************)
+
+
(* Add LoadPath ".." as SMTCoq. *)
Require Import Bool List Int63 PArray.
Require Import State SMT_terms.
diff --git a/src/extraction/Extract.v b/src/extraction/Extract.v
index 1161f48..2663fb3 100644
--- a/src/extraction/Extract.v
+++ b/src/extraction/Extract.v
@@ -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/extraction/extrNative.ml b/src/extraction/extrNative.ml
index 4d56287..d8d1265 100644
--- a/src/extraction/extrNative.ml
+++ b/src/extraction/extrNative.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 *)
+(* *)
+(**************************************************************************)
+
+
type comparison = Eq | Lt | Gt
type 'a carry = C0 of 'a | C1 of 'a
diff --git a/src/extraction/extrNative.mli b/src/extraction/extrNative.mli
index 14eff5f..3f255bf 100644
--- a/src/extraction/extrNative.mli
+++ b/src/extraction/extrNative.mli
@@ -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 *)
+(* *)
+(**************************************************************************)
+
+
type comparison = Eq | Lt | Gt
type 'a carry = C0 of 'a | C1 of 'a
diff --git a/src/extraction/sat_checker.ml b/src/extraction/sat_checker.ml
index 59635e0..0ed36a3 100644
--- a/src/extraction/sat_checker.ml
+++ b/src/extraction/sat_checker.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 *)
+(* *)
+(**************************************************************************)
+
+
(** val negb : bool -> bool **)
let negb = function
diff --git a/src/extraction/sat_checker.mli b/src/extraction/sat_checker.mli
index 5fa2757..ed63e26 100644
--- a/src/extraction/sat_checker.mli
+++ b/src/extraction/sat_checker.mli
@@ -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 *)
+(* *)
+(**************************************************************************)
+
+
val negb : bool -> bool
type 'a list =
diff --git a/src/extraction/smt_checker.ml b/src/extraction/smt_checker.ml
index 53aa130..ed446b7 100644
--- a/src/extraction/smt_checker.ml
+++ b/src/extraction/smt_checker.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 *)
+(* *)
+(**************************************************************************)
+
+
type __ = Obj.t
let __ = let rec f _ = Obj.repr f in Obj.repr f
diff --git a/src/extraction/smt_checker.mli b/src/extraction/smt_checker.mli
index 502d6f3..2fbf9b8 100644
--- a/src/extraction/smt_checker.mli
+++ b/src/extraction/smt_checker.mli
@@ -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 *)
+(* *)
+(**************************************************************************)
+
+
type __ = Obj.t
type unit0 =
diff --git a/src/extraction/smtcoq.ml b/src/extraction/smtcoq.ml
index f3bd6b1..07ed9a3 100644
--- a/src/extraction/smtcoq.ml
+++ b/src/extraction/smtcoq.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 *)
+(* *)
+(**************************************************************************)
+
+
type solver = Zchaff | Verit
diff --git a/src/extraction/test.ml b/src/extraction/test.ml
index 0b16b7f..f91a661 100644
--- a/src/extraction/test.ml
+++ b/src/extraction/test.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 *)
+(* *)
+(**************************************************************************)
+
+
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat1.cnf\" \"tests/sat1.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat1.cnf" "tests/sat1.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat2.cnf\" \"tests/sat2.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat2.cnf" "tests/sat2.zlog")
let _ = Printf.printf "Zchaff_checker.checker \"tests/sat3.cnf\" \"tests/sat3.zlog\" = %b\n" (Zchaff_checker.checker "tests/sat3.cnf" "tests/sat3.zlog")
diff --git a/src/extraction/verit_checker.ml b/src/extraction/verit_checker.ml
index e317dcf..20040bc 100644
--- a/src/extraction/verit_checker.ml
+++ b/src/extraction/verit_checker.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 SmtMisc
open SmtCertif
open SmtForm
diff --git a/src/extraction/zchaff_checker.ml b/src/extraction/zchaff_checker.ml
index 79e87cc..60d0a38 100644
--- a/src/extraction/zchaff_checker.ml
+++ b/src/extraction/zchaff_checker.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 SmtCertif
open SmtForm
open SatAtom
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
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index 533f139..ea5a42a 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.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 Smtlib2_ast
open SmtAtom
open SmtForm
diff --git a/src/spl/Arithmetic.v b/src/spl/Arithmetic.v
index a3e3162..8ec41ab 100644
--- a/src/spl/Arithmetic.v
+++ b/src/spl/Arithmetic.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 *)
(* *)
(**************************************************************************)
+
(*** Spl -- a small checker for simplifications ***)
(* Add LoadPath ".." as SMTCoq. *)
diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index 90483db..f7e011b 100644
--- a/src/spl/Operators.v
+++ b/src/spl/Operators.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 *)
(* *)
(**************************************************************************)
+
(*** Spl -- a small checker for simplifications ***)
(* Add LoadPath ".." as SMTCoq. *)
diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v
index 1da19aa..fba6657 100644
--- a/src/spl/Syntactic.v
+++ b/src/spl/Syntactic.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 *)
(* *)
(**************************************************************************)
+
(*** Spl -- a small checker for simplifications ***)
Require Import List PArray Bool Int63 ZMicromega.
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 *)
(* *)
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index d2db93e..48ae312 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.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/verit/veritLexer.mll b/src/verit/veritLexer.mll
index 3314fae..925ba92 100644
--- a/src/verit/veritLexer.mll
+++ b/src/verit/veritLexer.mll
@@ -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 VeritParser
exception Eof
diff --git a/src/verit/veritParser.mly b/src/verit/veritParser.mly
index f36b857..6bb9639 100644
--- a/src/verit/veritParser.mly
+++ b/src/verit/veritParser.mly
@@ -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 SmtAtom
open SmtForm
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 33c059d..97fbac6 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.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/verit/veritSyntax.mli b/src/verit/veritSyntax.mli
index 9813b54..cec2d97 100644
--- a/src/verit/veritSyntax.mli
+++ b/src/verit/veritSyntax.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 *)
(* *)
(**************************************************************************)
+
exception Sat
type typ = | Inpu | Deep | True | Fals | Andp | Andn | Orp | Orn | Xorp1 | Xorp2 | Xorn1 | Xorn2 | Impp | Impn1 | Impn2 | Equp1 | Equp2 | Equn1 | Equn2 | Itep1 | Itep2 | Iten1 | Iten2 | Eqre | Eqtr | Eqco | Eqcp | Dlge | Lage | Lata | Dlde | Lade | Fins | Eins | Skea | Skaa | Qnts | Qntm | Reso | And | Nor | Or | Nand | Xor1 | Xor2 | Nxor1 | Nxor2 | Imp | Nimp1 | Nimp2 | Equ1 | Equ2 | Nequ1 | Nequ2 | Ite1 | Ite2 | Nite1 | Nite2 | Tpal | Tlap | Tple | Tpne | Tpde | Tpsa | Tpie | Tpma | Tpbr | Tpbe | Tpsc | Tppp | Tpqt | Tpqs | Tpsk | Subp
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index 919f2f1..6eb1991 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.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/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index eb43cb0..373e8af 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -1,14 +1,14 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
(* from the PArray library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Cyclic63_standard.v b/src/versions/standard/Int63/Cyclic63_standard.v
index 54f2bbb..3033781 100644
--- a/src/versions/standard/Int63/Cyclic63_standard.v
+++ b/src/versions/standard/Int63/Cyclic63_standard.v
@@ -1,16 +1,23 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Chantal Keller *)
+(* *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
-(** * Int63 numbers defines indeed a cyclic structure : Z/(2^63)Z *)
-(**
-Author: Arnaud Spiwack (+ Pierre Letouzey)
-*)
+(** * Int63 numbers defines indeed a cyclic structure : Z/(2^63)Z *)
(* Add LoadPath "." as SMTCoq.versions.standard.Int63. *)
Require Import List.
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/versions/standard/Int63/Int63Axioms_standard.v
index 99a5496..83969ba 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/versions/standard/Int63/Int63Axioms_standard.v
@@ -1,14 +1,16 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Int63Lib_standard.v b/src/versions/standard/Int63/Int63Lib_standard.v
index 482144e..4d21346 100644
--- a/src/versions/standard/Int63/Int63Lib_standard.v
+++ b/src/versions/standard/Int63/Int63Lib_standard.v
@@ -1,12 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-(* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *)
-(************************************************************************)
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Chantal Keller *)
+(* *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
Require Import NaryFunctions.
Require Import Wf_nat.
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/versions/standard/Int63/Int63Native_standard.v
index 3f2c081..0431784 100644
--- a/src/versions/standard/Int63/Int63Native_standard.v
+++ b/src/versions/standard/Int63/Int63Native_standard.v
@@ -1,14 +1,16 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v
index 3a0dfae..f34260c 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/versions/standard/Int63/Int63Op_standard.v
@@ -1,14 +1,16 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Int63Properties_standard.v b/src/versions/standard/Int63/Int63Properties_standard.v
index 89851da..68c2729 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/versions/standard/Int63/Int63Properties_standard.v
@@ -1,14 +1,16 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Int63_standard.v b/src/versions/standard/Int63/Int63_standard.v
index 52be2c3..6b480b0 100644
--- a/src/versions/standard/Int63/Int63_standard.v
+++ b/src/versions/standard/Int63/Int63_standard.v
@@ -1,14 +1,16 @@
(**************************************************************************)
(* *)
(* SMTCoq *)
-(* Copyright (C) 2011 - 2015 *)
+(* Copyright (C) 2011 - 2016 *)
(* *)
(* Chantal Keller *)
(* *)
-(* from the Int63 library of native-coq *)
-(* by Benjamin Gregoire and Laurent Thery *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
(* *)
-(* 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/versions/standard/Int63/Ring63_standard.v b/src/versions/standard/Int63/Ring63_standard.v
index 7b9fc1f..7041c79 100644
--- a/src/versions/standard/Int63/Ring63_standard.v
+++ b/src/versions/standard/Int63/Ring63_standard.v
@@ -1,10 +1,21 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
+(**************************************************************************)
+(* *)
+(* SMTCoq *)
+(* Copyright (C) 2011 - 2016 *)
+(* *)
+(* Chantal Keller *)
+(* *)
+(* from the Int31 library *)
+(* by Arnaud Spiwack and Pierre Letouzey *)
+(* and the Int63 library of native-coq *)
+(* by Benjamin Gregoire and Laurent Thery *)
+(* *)
+(* Inria - École Polytechnique - Université Paris-Sud *)
+(* *)
+(* This file is distributed under the terms of the CeCILL-C licence *)
+(* *)
+(**************************************************************************)
+
(** * Int63 numbers defines Z/(2^63)Z, and can hence be equipped
with a ring structure and a ring tactic *)
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 66106a6..74c484a 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.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/zchaff/cnfParser.ml b/src/zchaff/cnfParser.ml
index 9a21675..c02211f 100644
--- a/src/zchaff/cnfParser.ml
+++ b/src/zchaff/cnfParser.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 SatParser
diff --git a/src/zchaff/satParser.ml b/src/zchaff/satParser.ml
index 731d499..79d0b14 100644
--- a/src/zchaff/satParser.ml
+++ b/src/zchaff/satParser.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 *)
(* *)
(**************************************************************************)
+
type lex_buff = {
buff : string;
mutable curr_char : int;
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 29891cc..ab260ba 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.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/zchaff/zchaffParser.ml b/src/zchaff/zchaffParser.ml
index c5bcb09..fa04dc6 100644
--- a/src/zchaff/zchaffParser.ml
+++ b/src/zchaff/zchaffParser.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 SatParser
open SmtForm
open SmtCertif