diff options
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 4 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 4 | ||||
| -rw-r--r-- | grammar/q_constr.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_coqast.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 2 | ||||
| -rw-r--r-- | grammar/q_util.mli | 2 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 2 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
8 files changed, 10 insertions, 10 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index fe0959ddbc..cb0f7d2d31 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 *) @@ -120,7 +120,7 @@ let make_possibly_empty_subentries loc s cl = let make_act loc act pil = let rec make = function - | [] -> <:expr< Pcoq.Gram.action (fun loc -> ($act$ : 'a)) >> + | [] -> <:expr< Pcoq.Gram.action (fun loc -> let loc = Compat.to_coqloc loc in ($act$ : 'a)) >> | GramNonTerminal (_,t,_,Some p) :: tl -> let p = Names.Id.to_string p in <:expr< diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 60ea0df026..71e5b8ae2c 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 6ae8bea3af..40db819494 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 dd97107f72..304e49923c 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 18b1ccd3be..a116b1e8b5 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 7393a0d588..a85ad2f6a6 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 66f82fcdfc..39f605e29c 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 03061d8bde..d789a6c1fc 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 *) |