From b6733f0507e3e04fb6130b3f82a79e8835e1062f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 31 May 2017 00:30:00 +0200
Subject: Bump year in headers.

---
 interp/constrarg.ml             | 2 +-
 interp/constrarg.mli            | 2 +-
 interp/constrexpr_ops.ml        | 2 +-
 interp/constrexpr_ops.mli       | 2 +-
 interp/constrextern.ml          | 2 +-
 interp/constrextern.mli         | 2 +-
 interp/constrintern.ml          | 2 +-
 interp/constrintern.mli         | 2 +-
 interp/coqlib.ml                | 2 +-
 interp/coqlib.mli               | 2 +-
 interp/dumpglob.ml              | 2 +-
 interp/dumpglob.mli             | 2 +-
 interp/genintern.ml             | 2 +-
 interp/genintern.mli            | 2 +-
 interp/implicit_quantifiers.ml  | 2 +-
 interp/implicit_quantifiers.mli | 2 +-
 interp/modintern.ml             | 2 +-
 interp/modintern.mli            | 2 +-
 interp/notation.ml              | 2 +-
 interp/notation.mli             | 2 +-
 interp/notation_ops.ml          | 2 +-
 interp/notation_ops.mli         | 2 +-
 interp/ppextend.ml              | 2 +-
 interp/ppextend.mli             | 2 +-
 interp/reserve.ml               | 2 +-
 interp/reserve.mli              | 2 +-
 interp/smartlocate.ml           | 2 +-
 interp/smartlocate.mli          | 2 +-
 interp/stdarg.ml                | 2 +-
 interp/stdarg.mli               | 2 +-
 interp/syntax_def.ml            | 2 +-
 interp/syntax_def.mli           | 2 +-
 interp/topconstr.ml             | 2 +-
 interp/topconstr.mli            | 2 +-
 34 files changed, 34 insertions(+), 34 deletions(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index ca828102b9..a9b3e45ec1 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.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/interp/constrarg.mli b/interp/constrarg.mli
index 6ccd944d43..c844d25253 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.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/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 04429851fd..033e19fc55 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.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/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index a92da035f6..ab01f15f45 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.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/interp/constrextern.ml b/interp/constrextern.ml
index 74504e36d4..848a78d33e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.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/interp/constrextern.mli b/interp/constrextern.mli
index f617faa38a..9e807f9618 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.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/interp/constrintern.ml b/interp/constrintern.ml
index 8400fdc967..57dec391dd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.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/interp/constrintern.mli b/interp/constrintern.mli
index 61e7c6f5cb..3867f90d6f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.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/interp/coqlib.ml b/interp/coqlib.ml
index 588637b76e..fca1971268 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.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/interp/coqlib.mli b/interp/coqlib.mli
index 5ba26d8286..2511901a75 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.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/interp/dumpglob.ml b/interp/dumpglob.ml
index b020f89457..13f592e000 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.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/interp/dumpglob.mli b/interp/dumpglob.mli
index e84a640521..0f114f04b4 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.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/interp/genintern.ml b/interp/genintern.ml
index d6bfd347ff..35a6098f09 100644
--- a/interp/genintern.ml
+++ b/interp/genintern.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/interp/genintern.mli b/interp/genintern.mli
index 4b244b38d8..d731e7bbd3 100644
--- a/interp/genintern.mli
+++ b/interp/genintern.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/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 10cfbe58fa..890d0dd034 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.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/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index d0327e5068..ac4523a78b 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.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/interp/modintern.ml b/interp/modintern.ml
index e5dce5ccf3..5c593b1a17 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.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/interp/modintern.mli b/interp/modintern.mli
index 1e04ada17b..a21b6e2312 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.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/interp/notation.ml b/interp/notation.ml
index 389a1c9dff..3310ed5794 100644
--- a/interp/notation.ml
+++ b/interp/notation.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/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..6ec3173d4e 100644
--- a/interp/notation.mli
+++ b/interp/notation.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/interp/notation_ops.ml b/interp/notation_ops.ml
index 5648821539..c46e5e9dac 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.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/interp/notation_ops.mli b/interp/notation_ops.mli
index c8fcbf7410..410f0673ba 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.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/interp/ppextend.ml b/interp/ppextend.ml
index 37bbe0ce87..56f08ca0ec 100644
--- a/interp/ppextend.ml
+++ b/interp/ppextend.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/interp/ppextend.mli b/interp/ppextend.mli
index de7a42eee5..4f36c10c0c 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.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/interp/reserve.ml b/interp/reserve.ml
index 388ca08050..537eba72a7 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.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/interp/reserve.mli b/interp/reserve.mli
index 9c77400da2..4fcef23c52 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.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/interp/smartlocate.ml b/interp/smartlocate.ml
index 478774219e..b686bc0c4a 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.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/interp/smartlocate.mli b/interp/smartlocate.mli
index 0749ca5769..718cb010f6 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.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/interp/stdarg.ml b/interp/stdarg.ml
index 2a7d52e3af..ea4d3ed22f 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.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/interp/stdarg.mli b/interp/stdarg.mli
index e1f648d7fc..c23902d5d7 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.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/interp/syntax_def.ml b/interp/syntax_def.ml
index 2523063e64..5bd337d432 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.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/interp/syntax_def.mli b/interp/syntax_def.mli
index 55e2848e69..36a3986b54 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.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/interp/topconstr.ml b/interp/topconstr.ml
index bf0ce60d88..277ffacd89 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.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/interp/topconstr.mli b/interp/topconstr.mli
index 58edd4ddf8..e723493198 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.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        *)
-- 
cgit v1.2.3


From 849bf3600fe11fea876c9aeea69fe806b0c8c5d8 Mon Sep 17 00:00:00 2001
From: Paul Steckler
Date: Fri, 9 Jun 2017 12:30:42 -0400
Subject: Fix Bug #5568, no dup notation warnings on repeated module imports

---
 interp/notation.ml     | 3 ++-
 interp/notation.mli    | 2 +-
 interp/notation_ops.ml | 9 ++++++++-
 3 files changed, 11 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/notation.ml b/interp/notation.ml
index 389a1c9dff..ba80cf1d2c 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -561,11 +561,12 @@ let interpretation_eq (vars1, t1) (vars2, t2) =
   List.equal var_attributes_eq vars1 vars2 &&
   Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2
 
-let exists_notation_in_scope scopt ntn r =
+let exists_notation_in_scope scopt ntn onlyprint r =
   let scope = match scopt with Some s -> s | None -> default_scope in
   try
     let sc = String.Map.find scope !scope_map in
     let n = String.Map.find ntn sc.notations in
+    onlyprint = n.not_onlyprinting && 
     interpretation_eq n.not_interp r
   with Not_found -> false
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..303fa8c7a0 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -142,7 +142,7 @@ val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
 
 (** Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
-      interpretation -> bool
+      bool -> interpretation -> bool
 
 (** Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope :
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 5648821539..26e61d13af 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -47,9 +47,16 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
     | GHole _ | GSort _ | GLetIn _), _
       -> false
 
+(* helper for NVar, NVar case in eq_notation_constr *)
+let get_var_ndx id vs = try Some (List.index Id.equal id vs) with Not_found -> None
+
 let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with
 | NRef gr1, NRef gr2 -> eq_gr gr1 gr2
-| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2)
+| NVar id1, NVar id2 -> (
+   match (get_var_ndx id1 vars1,get_var_ndx id2 vars2) with
+   | Some n,Some m -> Int.equal n m
+   | None  ,None   -> Id.equal id1 id2
+   | _             -> false)
 | NApp (t1, a1), NApp (t2, a2) ->
   (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2
 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *)
-- 
cgit v1.2.3