aboutsummaryrefslogtreecommitdiffstats
path: root/src/spl/Syntactic.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/spl/Syntactic.v')
-rw-r--r--src/spl/Syntactic.v5
1 files changed, 3 insertions, 2 deletions
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.