summaryrefslogtreecommitdiff
path: root/grammar
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-01-26 16:56:33 +0100
commit164c6861860e6b52818c031f901ffeff91fca16a (patch)
tree4f91d20c890c25915e7b28226c663b94a8cfb0d3 /grammar
parent91dbeab8eef959c3f64960909ca69d4e68c8198d (diff)
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'grammar')
-rw-r--r--grammar/argextend.ml42
-rw-r--r--grammar/grammar.mllib4
-rw-r--r--grammar/q_constr.ml42
-rw-r--r--grammar/q_coqast.ml42
-rw-r--r--grammar/q_util.ml42
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--grammar/vernacextend.ml42
8 files changed, 9 insertions, 9 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index fe0959dd..8def9537 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index 60ea0df0..71e5b8ae 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -16,13 +16,13 @@ Backtrace
Pp_control
Flags
Loc
+CList
+CString
Serialize
Stateid
Feedback
Pp
-CList
-CString
CArray
CStack
Util
diff --git a/grammar/q_constr.ml4 b/grammar/q_constr.ml4
index 6ae8bea3..40db8194 100644
--- a/grammar/q_constr.ml4
+++ b/grammar/q_constr.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index dd97107f..304e4992 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4
index 18b1ccd3..a116b1e8 100644
--- a/grammar/q_util.ml4
+++ b/grammar/q_util.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 7393a0d5..a85ad2f6 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 66f82fcd..39f605e2 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index 03061d8b..d789a6c1 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <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 *)