Imported Upstream version 8.3.pl3upstream/8.3.pl3

43 files changed, 126 insertions, 115 deletions

diff --git a/parsing/argextend.ml4 b/parsing/argextend.ml4
index 8bc7ad02..848223a0 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: argextend.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: argextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Genarg
 open Q_util
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 943a9487..ba965a54 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: egrammar.ml 14779 2011-12-07 21:54:18Z herbelin $ *)
 
 open Pp
 open Util
@@ -169,24 +169,27 @@ let pure_sublevels level symbs =
       failwith "") symbs
 
 let extend_constr (entry,level) (n,assoc) mkact forpat rules =
-  List.iter (fun pt ->
+  List.fold_left (fun nb pt ->
   let symbs = make_constr_prod_item assoc n forpat pt in
   let pure_sublevels = pure_sublevels level symbs in
   let needed_levels = register_empty_levels forpat pure_sublevels in
   let pos,p4assoc,name,reinit = find_position forpat assoc level in
+  let nb_decls = List.length needed_levels + 1 in
   List.iter (prepare_empty_levels forpat) needed_levels;
-  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])]) rules
+  grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact pt])];
+  nb_decls) 0 rules
 
 let extend_constr_notation (n,assoc,ntn,rules) =
   (* Add the notation in constr *)
   let mkact loc env = CNotation (loc,ntn,env) in
   let e = interp_constr_entry_key false (ETConstr (n,())) in
-  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules;
+  let nb = extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rules in
   (* Add the notation in cases_pattern *)
   let mkact loc env = CPatNotation (loc,ntn,env) in
   let e = interp_constr_entry_key true (ETConstr (n,())) in
-  extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
-    true rules
+  let nb' =
+    extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact) true rules in
+  nb+nb'
 
 (**********************************************************************)
 (** Making generic actions in type generic_argument                   *)
@@ -273,7 +276,8 @@ let add_tactic_entry (key,lev,prods,tac) =
 	(TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in
       make_rule univ (mkact key tac) make_prod_item prods in
   synchronize_level_positions ();
-  grammar_extend entry pos None [(None, None, List.rev [rules])]
+  grammar_extend entry pos None [(None, None, List.rev [rules])];
+  1
 
 (**********************************************************************)
 (** State of the grammar extensions                                   *)
@@ -290,17 +294,17 @@ type all_grammar_command =
       (string * int * grammar_prod_item list *
          (dir_path * Tacexpr.glob_tactic_expr))
 
-let (grammar_state : all_grammar_command list ref) = ref []
+let (grammar_state : (int * all_grammar_command) list ref) = ref []
 
 let extend_grammar gram =
-  (match gram with
+  let nb = match gram with
   | Notation (_,_,a) -> extend_constr_notation a
-  | TacticGrammar g -> add_tactic_entry g);
-  grammar_state := gram :: !grammar_state
+  | TacticGrammar g -> add_tactic_entry g in
+  grammar_state := (nb,gram) :: !grammar_state
 
 let recover_notation_grammar ntn prec =
   let l = map_succeed (function
-    | Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
+    | _, Notation (prec',vars,(_,_,ntn',_ as x)) when prec = prec' & ntn = ntn' ->
 	 vars, x
     | _ ->
 	 failwith "") !grammar_state in
@@ -320,11 +324,7 @@ let factorize_grams l1 l2 =
   if l1 == l2 then ([], [], l1) else list_share_tails l1 l2
 
 let number_of_entries gcl =
-  List.fold_left
-    (fun n -> function
-      | Notation _ -> n + 2 (* 1 for operconstr, 1 for pattern *)
-      | TacticGrammar _ -> n + 1)
-    0 gcl
+  List.fold_left (fun n (p,_) -> n + p) 0 gcl
 
 let unfreeze (grams, lex) =
   let (undo, redo, common) = factorize_grams !grammar_state grams in
@@ -333,7 +333,7 @@ let unfreeze (grams, lex) =
   remove_levels n;
   grammar_state := common;
   Lexer.unfreeze lex;
-  List.iter extend_grammar (List.rev redo)
+  List.iter extend_grammar (List.rev (List.map snd redo))
 
 let init_grammar () =
   remove_grammars (number_of_entries !grammar_state);
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index f6b9f6ad..8554c9be 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: egrammar.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: egrammar.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 92ca4dd1..9b85ada5 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extend.ml 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: extend.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 
diff --git a/parsing/extend.mli b/parsing/extend.mli
index ad371872..269331c2 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extend.mli 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: extend.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 
diff --git a/parsing/extrawit.ml b/parsing/extrawit.ml
index e12e2593..94179d95 100644
--- a/parsing/extrawit.ml
+++ b/parsing/extrawit.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extrawit.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extrawit.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Genarg
diff --git a/parsing/extrawit.mli b/parsing/extrawit.mli
index 1a1b6fe4..9b0aac39 100644
--- a/parsing/extrawit.mli
+++ b/parsing/extrawit.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extrawit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extrawit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Genarg
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 76b761b1..e7d4684b 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_constr.ml4 13359 2010-07-30 08:46:55Z herbelin $ *)
+(* $Id: g_constr.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Pcoq
diff --git a/parsing/g_decl_mode.ml4 b/parsing/g_decl_mode.ml4
index 0aa8272b..8893ebcc 100644
--- a/parsing/g_decl_mode.ml4
+++ b/parsing/g_decl_mode.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: g_decl_mode.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_decl_mode.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 open Decl_expr
diff --git a/parsing/g_intsyntax.mli b/parsing/g_intsyntax.mli
index 0713d47b..de85b6af 100644
--- a/parsing/g_intsyntax.mli
+++ b/parsing/g_intsyntax.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \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 e0f31b98..dac4a135 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_ltac.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_ltac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
index 21335332..d3f12bed 100644
--- a/parsing/g_natsyntax.mli
+++ b/parsing/g_natsyntax.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: g_natsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: g_natsyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* Nice syntax for naturals. *)
 
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index a7ed810d..c4fd3bb5 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(*i $Id: g_prim.ml4 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: g_prim.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pcoq
 open Names
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index df23465e..f1dad3b2 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_proofs.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_proofs.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 open Pcoq
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 4a1b9c63..be20f891 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_tactic.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_tactic.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Pcoq
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a00bb689..d761ed64 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,7 +9,7 @@
 (*i camlp4deps: "parsing/grammar.cma" i*)
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_vernac.ml4 13699 2010-12-09 19:24:45Z herbelin $ *)
+(* $Id: g_vernac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 
 open Pp
diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4
index 5ad9f664..b8fee3ff 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo" i*)
 
-(* $Id: g_xml.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_xml.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
index 16b1ba65..05c161c2 100644
--- a/parsing/g_zsyntax.mli
+++ b/parsing/g_zsyntax.mli
@@ -1,11 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: g_zsyntax.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: g_zsyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (* Nice syntax for integers. *)
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index a89594c2..50349e22 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@
 (* Add pr_o.cmo to circumvent a useless-warning bug when preprocessed with
  * ast-based camlp4 *)
 
-(*i $Id: lexer.ml4 13521 2010-10-10 21:59:00Z herbelin $ i*)
+(*i $Id: lexer.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index a25774c5..93fc4231 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: lexer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: lexer.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 14d50e6c..ff5213ef 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo pa_macro.cmo" i*)
 
-(*i $Id: pcoq.ml4 13690 2010-12-06 16:15:54Z glondu $ i*)
+(*i $Id: pcoq.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 4eb06088..61d8f4f6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.mli 13690 2010-12-06 16:15:54Z glondu $ i*)
+(*i $Id: pcoq.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index eef28fcf..bcca937b 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppconstr.ml 13358 2010-07-29 23:10:17Z herbelin $ *)
+(* $Id: ppconstr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Util
@@ -254,7 +254,7 @@ let pr_binder_among_many pr_c = function
       let c,topt = match c with
         | CCast(_,c, CastConv (_,t)) -> c, t
         | _ -> c, CHole (dummy_loc, None) in
-      hov 1 (pr_lname na ++ pr_opt_type pr_c topt ++
+      surround (pr_lname na ++ pr_opt_type pr_c topt ++
          str":=" ++ cut() ++ pr_c c)
 
 let pr_undelimited_binders sep pr_c =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index 1ad110cb..d27b318a 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ppconstr.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ppconstr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Environ
diff --git a/parsing/ppdecl_proof.ml b/parsing/ppdecl_proof.ml
index 275b02df..c0eddcc5 100644
--- a/parsing/ppdecl_proof.ml
+++ b/parsing/ppdecl_proof.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppdecl_proof.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ppdecl_proof.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Pp
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index f27959c2..f63d6659 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pptactic.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: pptactic.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Names
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index bb9d8426..40880f58 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pptactic.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: pptactic.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Genarg
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b5e0cc4a..44ac445d 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: ppvernac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: ppvernac.ml 14657 2011-11-16 08:46:33Z herbelin $ *)
 
 open Pp
 open Names
@@ -439,8 +439,8 @@ let pr_paren_reln_or_extern = function
 
 let pr_statement head (id,(bl,c,guard)) =
   assert (id<>None);
-  hov 0
-    (head ++ pr_lident (Option.get id) ++ spc() ++
+  hov 1
+    (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
     pr_opt (pr_guard_annot bl) guard ++
     str":" ++ pr_spc_lconstr c)
diff --git a/parsing/ppvernac.mli b/parsing/ppvernac.mli
index dce1bbd7..e63cf7b0 100644
--- a/parsing/ppvernac.mli
+++ b/parsing/ppvernac.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ppvernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ppvernac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Pp
 open Genarg
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml
index 3fc18219..ea97a198 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@
  * on May-June 2006 for implementation of abstraction of pretty-printing of objects.
  *)
 
-(* $Id: prettyp.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
+(* $Id: prettyp.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/prettyp.mli b/parsing/prettyp.mli
index 5704f54e..fef66a63 100644
--- a/parsing/prettyp.mli
+++ b/parsing/prettyp.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: prettyp.mli 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: prettyp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/printer.ml b/parsing/printer.ml
index cf0050a5..75cdead9 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: printer.ml 13390 2010-09-02 08:03:01Z herbelin $ *)
+(* $Id: printer.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
@@ -499,14 +499,26 @@ let pr_prim_rule = function
 let prterm = pr_lconstr
 
 
-(* spiwack: printer function for sets of Environ.assumption.
-            It is used primarily by the Print Assumption command. *)
+(* Printer function for sets of Assumptions.assumptions.
+   It is used primarily by the Print Assumptions command. *)
+
+open Assumptions
+
 let pr_assumptionset env s =
-  if (Environ.ContextObjectMap.is_empty s) then
-    str "Closed under the global context"
+  if ContextObjectMap.is_empty s then
+    str "Closed under the global context" ++ fnl()
   else
+    let safe_pr_constant env kn =
+      try pr_constant env kn
+      with Not_found ->
+	let mp,_,lab = repr_con kn in
+	str (string_of_mp mp ^ "." ^ string_of_label lab)
+    in
+    let safe_pr_ltype typ =
+      try str " : " ++ pr_ltype typ with _ -> mt ()
+    in
     let (vars,axioms,opaque) =
-      Environ.ContextObjectMap.fold (fun t typ r ->
+      ContextObjectMap.fold (fun t typ r ->
 	let (v,a,o) = r in
 	match t with
 	| Variable id -> (  Some (
@@ -521,9 +533,8 @@ let pr_assumptionset env s =
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
-			   ++ (pr_constant env kn)
-	                   ++ str " : "
-	                   ++ pr_ltype typ
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
 	                   ++ fnl ()
 			     )
 			 , o
@@ -531,9 +542,8 @@ let pr_assumptionset env s =
 	| Opaque kn    -> ( v , a ,
 			     Some (
 			      Option.default (fnl ()) o
-			   ++ (pr_constant env kn)
-	                   ++ str " : "
-	                   ++ pr_ltype typ
+			   ++ safe_pr_constant env kn
+	                   ++ safe_pr_ltype typ
 	                   ++ fnl ()
 			     )
 			 )
diff --git a/parsing/printer.mli b/parsing/printer.mli
index a6f73a40..99ab3ca3 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: printer.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -131,7 +131,8 @@ val prterm                 : constr -> std_ppcmds (* = pr_lconstr *)
 
 (* spiwack: printer function for sets of Environ.assumption.
             It is used primarily by the Print Assumption command. *)
-val pr_assumptionset : env -> Term.types Environ.ContextObjectMap.t ->std_ppcmds
+val pr_assumptionset :
+  env -> Term.types Assumptions.ContextObjectMap.t ->std_ppcmds
 
 
 type printer_pr = {
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index 16f6e6c9..6339ed8f 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \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 85cfe1a1..77ff34f1 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \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 fff29083..3d203dbe 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: q_constr.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: q_constr.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Rawterm
 open Term
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index d0afcdd4..d612dd55 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "q_MLast.cmo pa_macro.cmo" i*)
 
-(* $Id: q_coqast.ml4 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: q_coqast.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/parsing/q_util.ml4 b/parsing/q_util.ml4
index 6d6c229c..a41824d0 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "q_MLast.cmo" i*)
 
-(* $Id: q_util.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: q_util.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (* This file defines standard combinators to build ml expressions *)
 
diff --git a/parsing/q_util.mli b/parsing/q_util.mli
index c55d8482..878adba6 100644
--- a/parsing/q_util.mli
+++ b/parsing/q_util.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: q_util.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: q_util.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 val patt_of_expr : MLast.expr -> MLast.patt
 
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index 39477b0b..0d7a9cfe 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: tacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
+(* $Id: tacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Genarg
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml
index 3d048c30..45816856 100644
--- a/parsing/tactic_printer.ml
+++ b/parsing/tactic_printer.ml
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tactic_printer.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tactic_printer.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/parsing/tactic_printer.mli b/parsing/tactic_printer.mli
index 9233233f..05ba20e9 100644
--- a/parsing/tactic_printer.mli
+++ b/parsing/tactic_printer.mli
@@ -1,12 +1,12 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactic_printer.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tactic_printer.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/parsing/vernacextend.ml4 b/parsing/vernacextend.ml4
index 860110e5..3f60aafa 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-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (*i camlp4use: "pa_extend.cmo q_MLast.cmo" i*)
 
-(* $Id: vernacextend.ml4 13799 2011-01-25 17:38:40Z glondu $ *)
+(* $Id: vernacextend.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Genarg