Imported Upstream version 8.4pl4dfsgupstream/8.4pl4dfsg

40 files changed, 62 insertions, 55 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 214a6b98..1fc429c6 100644
--- a/parsing/argextend.ml4
+++ b/parsing/argextend.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,7 +32,7 @@ let rec make_rawwit loc = function
   | ConstrMayEvalArgType -> <:expr< Genarg.rawwit_constr_may_eval >>
   | QuantHypArgType -> <:expr< Genarg.rawwit_quant_hyp >>
   | RedExprArgType -> <:expr< Genarg.rawwit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.rawwit_open_constr_gen $mlexpr_of_bool b$ >>
+  | OpenConstrArgType (b1,b2) -> <:expr< Genarg.rawwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.rawwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.rawwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_rawwit loc t$ >>
@@ -62,7 +62,7 @@ let rec make_globwit loc = function
   | ConstrArgType -> <:expr< Genarg.globwit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.globwit_constr_may_eval >>
   | RedExprArgType -> <:expr< Genarg.globwit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.globwit_open_constr_gen $mlexpr_of_bool b$ >>
+  | OpenConstrArgType (b1,b2) -> <:expr< Genarg.globwit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.globwit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.globwit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_globwit loc t$ >>
@@ -92,7 +92,7 @@ let rec make_wit loc = function
   | ConstrArgType -> <:expr< Genarg.wit_constr >>
   | ConstrMayEvalArgType -> <:expr< Genarg.wit_constr_may_eval >>
   | RedExprArgType -> <:expr< Genarg.wit_red_expr >>
-  | OpenConstrArgType b -> <:expr< Genarg.wit_open_constr_gen $mlexpr_of_bool b$ >>
+  | OpenConstrArgType (b1,b2) -> <:expr< Genarg.wit_open_constr_gen ($mlexpr_of_bool b1$,$mlexpr_of_bool b2$) >>
   | ConstrWithBindingsArgType -> <:expr< Genarg.wit_constr_with_bindings >>
   | BindingsArgType -> <:expr< Genarg.wit_bindings >>
   | List0ArgType t -> <:expr< Genarg.wit_list0 $make_wit loc t$ >>
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 12359776..6deb7622 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index f04809ce..094b4203 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 0a76829b..620e2ac2 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/extend.mli b/parsing/extend.mli
index f63123cd..dd8ed0cd 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index 75f6a7de..aaf64523 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 8cd162c9..d8f36928 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 22dc427b..325c1cec 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index d082b91c..34615ad1 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index 6fee4e1f..e0aae9a6 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 8a6f67c4..557972ce 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 1609e541..820a1f16 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -198,7 +198,7 @@ let merge_occurrences loc cl = function
 
 GEXTEND Gram
   GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
-  bindings red_expr int_or_var open_constr casted_open_constr
+  bindings red_expr int_or_var open_constr casted_open_constr open_constr_wTC
   simple_intropattern;
 
   int_or_var:
@@ -219,6 +219,9 @@ GEXTEND Gram
   open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
+  open_constr_wTC:
+    [ [ c = constr -> ((),c) ] ]
+  ;
   casted_open_constr:
     [ [ c = constr -> ((),c) ] ]
   ;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 301370e7..75cd7d67 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -414,7 +414,7 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | IDENT "Include"; e = module_expr_inl; l = LIST0 ext_module_expr ->
+      | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
 	  VernacInclude(e::l)
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
 	  Flags.if_verbose
@@ -842,6 +842,7 @@ GEXTEND Gram
          -> PrintCoercionPaths (s,t)
       | IDENT "Canonical"; IDENT "Projections" -> PrintCanonicalConversions
       | IDENT "Tables" -> PrintTables
+      | IDENT "Options" -> PrintTables (* A Synonymous to Tables *)
       | IDENT "Hint" -> PrintHintGoal
       | IDENT "Hint"; qid = smart_global -> PrintHint qid
       | IDENT "Hint"; "*" -> PrintHintDb
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 869674f4..6f5e378a 100644
--- a/parsing/g_xml.ml4
+++ b/parsing/g_xml.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index c8e67f4d..82ae2dc8 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index a0820f55..cb6b694c 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7f11af93..7949a77d 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -380,9 +380,11 @@ module Tactic =
     (* Entries that can be refered via the string -> Gram.entry table *)
     (* Typically for tactic user extensions *)
     let open_constr =
-      make_gen_entry utactic (rawwit_open_constr_gen false) "open_constr"
+      make_gen_entry utactic (rawwit_open_constr_gen (false,false)) "open_constr"
     let casted_open_constr =
-      make_gen_entry utactic (rawwit_open_constr_gen true) "casted_open_constr"
+      make_gen_entry utactic (rawwit_open_constr_gen (true,false)) "casted_open_constr"
+    let open_constr_wTC =
+      make_gen_entry utactic (rawwit_open_constr_gen (false,true)) "open_constr_wTC"
     let constr_with_bindings =
       make_gen_entry utactic rawwit_constr_with_bindings "constr_with_bindings"
     let bindings =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 53c317c0..1b04b117 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -211,6 +211,7 @@ module Tactic :
   sig
     open Glob_term
     val open_constr : open_constr_expr Gram.entry
+    val open_constr_wTC : open_constr_expr Gram.entry
     val casted_open_constr : open_constr_expr Gram.entry
     val constr_with_bindings : constr_expr with_bindings Gram.entry
     val bindings : constr_expr bindings Gram.entry
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 5405e523..4fde091d 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 7a24eb9f..bc3a6668 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 17ef9f85..fa573c8a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -149,7 +149,7 @@ let rec pr_raw_generic prc prlc prtac prpat prref (x:Genarg.rlevel Genarg.generi
   | RedExprArgType ->
       pr_red_expr (prc,prlc,pr_or_by_notation prref,prpat)
         (out_gen rawwit_red_expr x)
-  | OpenConstrArgType b -> prc (snd (out_gen (rawwit_open_constr_gen b) x))
+  | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (rawwit_open_constr_gen (b1,b2)) x))
   | ConstrWithBindingsArgType ->
       pr_with_bindings prc prlc (out_gen rawwit_constr_with_bindings x)
   | BindingsArgType ->
@@ -195,7 +195,7 @@ let rec pr_glob_generic prc prlc prtac prpat x =
       pr_red_expr
         (prc,prlc,pr_or_var (pr_and_short_name pr_evaluable_reference),prpat)
         (out_gen globwit_red_expr x)
-  | OpenConstrArgType b -> prc (snd (out_gen (globwit_open_constr_gen b) x))
+  | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (globwit_open_constr_gen (b1,b2)) x))
   | ConstrWithBindingsArgType ->
       pr_with_bindings prc prlc (out_gen globwit_constr_with_bindings x)
   | BindingsArgType ->
@@ -236,7 +236,7 @@ let rec pr_generic prc prlc prtac prpat x =
   | RedExprArgType ->
       pr_red_expr (prc,prlc,pr_evaluable_reference,prpat)
         (out_gen wit_red_expr x)
-  | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x))
+  | OpenConstrArgType (b1,b2) -> prc (snd (out_gen (wit_open_constr_gen (b1,b2)) x))
   | ConstrWithBindingsArgType ->
       let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in
       pr_with_bindings prc prlc (c,b)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 0f82071d..c5953da1 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index f2491293..98c02567 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index 6d381c72..87b4fe56 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 99e10908..3b3fb2c3 100644
--- a/parsing/prettyp.ml
+++ b/parsing/prettyp.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 84de2074..4cf3e489 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/printer.ml b/parsing/printer.ml
index a5bd30b1..1b887e6e 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -205,10 +205,10 @@ let pr_var_decl env (id,c,typ) =
     | None ->  (mt ())
     | Some c ->
 	(* Force evaluation *)
-	let pb = pr_lconstr_env env c in
+	let pb = pr_lconstr_core true env c in
 	let pb = if isCast c then surround pb else pb in
 	(str" := " ++ pb ++ cut () ) in
-  let pt = pr_ltype_env env typ in
+  let pt = pr_ltype_core true env typ in
   let ptyp = (str" : " ++ pt) in
   (pr_id id ++ hov 0 (pbody ++ ptyp))
 
@@ -217,10 +217,10 @@ let pr_rel_decl env (na,c,typ) =
     | None -> mt ()
     | Some c ->
 	(* Force evaluation *)
-	let pb = pr_lconstr_env env c in
+	let pb = pr_lconstr_core true env c in
 	let pb = if isCast c then surround pb else pb in
 	(str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = pr_ltype_env env typ in
+  let ptyp = pr_ltype_core true env typ in
   match na with
   | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
   | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 3abe90e7..c0ef1932 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index b46cf42d..ad791de9 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/printmod.mli b/parsing/printmod.mli
index 17ad6b25..f60d19b3 100644
--- a/parsing/printmod.mli
+++ b/parsing/printmod.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
index dfe7d9c0..7e69163e 100644
--- a/parsing/q_constr.ml4
+++ b/parsing/q_constr.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 02311fe4..f5508352 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -189,7 +189,7 @@ let rec mlexpr_of_argtype loc = function
   | Genarg.VarArgType -> <:expr< Genarg.VarArgType >>
   | Genarg.StringArgType -> <:expr< Genarg.StringArgType >>
   | Genarg.QuantHypArgType -> <:expr< Genarg.QuantHypArgType >>
-  | Genarg.OpenConstrArgType b -> <:expr< Genarg.OpenConstrArgType $mlexpr_of_bool b$ >>
+  | Genarg.OpenConstrArgType (b1,b2) -> <:expr< Genarg.OpenConstrArgType ($mlexpr_of_bool b1$, $mlexpr_of_bool b2$) >>
   | Genarg.ConstrWithBindingsArgType -> <:expr< Genarg.ConstrWithBindingsArgType >>
   | Genarg.BindingsArgType -> <:expr< Genarg.BindingsArgType >>
   | Genarg.RedExprArgType -> <:expr< Genarg.RedExprArgType >>
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 7fe5a3c4..947e7e54 100644
--- a/parsing/q_util.ml4
+++ b/parsing/q_util.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index 527cc6b2..babbfb8a 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 77364180..7bcd1cf2 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index eaab1445..9355a2a5 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 1c045e62..2348706f 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/tok.ml b/parsing/tok.ml
index cf24aa5f..5b9aed6d 100644
--- a/parsing/tok.ml
+++ b/parsing/tok.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/tok.mli b/parsing/tok.mli
index a1ecd2c6..50a51198 100644
--- a/parsing/tok.mli
+++ b/parsing/tok.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index bcdf7cff..1df5fbbd 100644
--- a/parsing/vernacextend.ml4
+++ b/parsing/vernacextend.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)