diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 2 | ||||
| -rw-r--r-- | checker/check_stat.ml | 2 | ||||
| -rw-r--r-- | checker/check_stat.mli | 2 | ||||
| -rw-r--r-- | checker/checker.ml | 2 | ||||
| -rw-r--r-- | checker/cic.mli | 2 | ||||
| -rw-r--r-- | checker/closure.ml | 2 | ||||
| -rw-r--r-- | checker/closure.mli | 2 | ||||
| -rw-r--r-- | checker/indtypes.ml | 2 | ||||
| -rw-r--r-- | checker/indtypes.mli | 2 | ||||
| -rw-r--r-- | checker/inductive.ml | 2 | ||||
| -rw-r--r-- | checker/inductive.mli | 2 | ||||
| -rw-r--r-- | checker/mod_checking.mli | 2 | ||||
| -rw-r--r-- | checker/modops.ml | 2 | ||||
| -rw-r--r-- | checker/modops.mli | 2 | ||||
| -rw-r--r-- | checker/print.ml | 2 | ||||
| -rw-r--r-- | checker/reduction.ml | 2 | ||||
| -rw-r--r-- | checker/reduction.mli | 2 | ||||
| -rw-r--r-- | checker/safe_typing.ml | 2 | ||||
| -rw-r--r-- | checker/safe_typing.mli | 2 | ||||
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/subtyping.mli | 2 | ||||
| -rw-r--r-- | checker/term.ml | 2 | ||||
| -rw-r--r-- | checker/type_errors.ml | 2 | ||||
| -rw-r--r-- | checker/type_errors.mli | 2 | ||||
| -rw-r--r-- | checker/typeops.ml | 2 | ||||
| -rw-r--r-- | checker/typeops.mli | 2 | ||||
| -rw-r--r-- | checker/univ.ml | 2 | ||||
| -rw-r--r-- | checker/univ.mli | 2 | ||||
| -rw-r--r-- | checker/validate.ml | 2 | ||||
| -rw-r--r-- | checker/values.ml | 4 | ||||
| -rw-r--r-- | checker/votour.ml | 2 |
31 files changed, 32 insertions, 32 deletions
diff --git a/checker/check.ml b/checker/check.ml index 8b299bf2a2..0ee88bc991 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/check_stat.ml b/checker/check_stat.ml index 741f532848..9751b45975 100644 --- a/checker/check_stat.ml +++ b/checker/check_stat.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/check_stat.mli b/checker/check_stat.mli index 39e19d10e4..cfa1e7b067 100644 --- a/checker/check_stat.mli +++ b/checker/check_stat.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/checker.ml b/checker/checker.ml index 8dbb7e0119..e9214f84e3 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/cic.mli b/checker/cic.mli index 3645587554..95461f15e7 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/closure.ml b/checker/closure.ml index cef1d31a68..8216665d42 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/closure.mli b/checker/closure.mli index 8b1f246c28..b99de64949 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 9ccaaa7cbb..1e1e255dfb 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 071eecbbcd..7eaaf65f22 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/inductive.ml b/checker/inductive.ml index c4ffc141ff..92b72b3b0b 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/inductive.mli b/checker/inductive.mli index ed3a7b53ce..ece8351744 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 5c7b392ffd..16a3792aa1 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/modops.ml b/checker/modops.ml index b720fb6213..bf30ade5a0 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/modops.mli b/checker/modops.mli index 26a088f32b..0efff63c82 100644 --- a/checker/modops.mli +++ b/checker/modops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/print.ml b/checker/print.ml index 7ef752b002..84c327941e 100644 --- a/checker/print.ml +++ b/checker/print.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/reduction.ml b/checker/reduction.ml index ec16aa2615..085a544c8a 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/reduction.mli b/checker/reduction.mli index 15a2df1f14..d0fa40e62d 100644 --- a/checker/reduction.mli +++ b/checker/reduction.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index 11cd742ba4..bb7640088c 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli index 8724f8e014..0eaeb1243c 100644 --- a/checker/safe_typing.mli +++ b/checker/safe_typing.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 7eae9b8310..c0f1a12a84 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/subtyping.mli b/checker/subtyping.mli index cc66fc5382..b1cfac2781 100644 --- a/checker/subtyping.mli +++ b/checker/subtyping.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/term.ml b/checker/term.ml index 591348cb69..51ba35ae4d 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/type_errors.ml b/checker/type_errors.ml index b7718e02da..c5a69efdcd 100644 --- a/checker/type_errors.ml +++ b/checker/type_errors.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/type_errors.mli b/checker/type_errors.mli index d9d1479580..b5f14c7189 100644 --- a/checker/type_errors.mli +++ b/checker/type_errors.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/typeops.ml b/checker/typeops.ml index 173e19ce1b..d22b8097be 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/typeops.mli b/checker/typeops.mli index db8e467a33..2be461b052 100644 --- a/checker/typeops.mli +++ b/checker/typeops.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/univ.ml b/checker/univ.ml index 668f3a0584..b585471a65 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/univ.mli b/checker/univ.mli index 7d4c629ab9..cbb4f95661 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/validate.ml b/checker/validate.ml index c434ef09d3..8200405878 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/checker/values.ml b/checker/values.ml index c175aed680..434cc85645 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 6466d8cc443b5896cb905776df0cc49e checker/cic.mli +MD5 075f580a0552808551d9cf5098435804 checker/cic.mli *) diff --git a/checker/votour.ml b/checker/votour.ml index 48f9f45e7e..9e35c7e5b2 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |