Imported Upstream version 8.4dfsgupstream/8.4dfsg

56 files changed, 462 insertions, 239 deletions

diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index f4dab15f..3690b924 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 076a946a..1eaf6b76 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 9258a39f..10709abc 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index dd50cda5..3ce8459b 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml
index 24a056d7..912d694e 100644
--- a/toplevel/backtrack.ml
+++ b/toplevel/backtrack.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -33,12 +33,18 @@ type info = {
   nproofs : int;
   prfname : identifier option;
   prfdepth : int;
+  ngoals : int;
   cmd : vernac_expr;
   mutable reachable : bool;
 }
 
 let history : info Stack.t = Stack.create ()
 
+(** Is this stack active (i.e. nonempty) ?
+    The stack is currently inactive when compiling files (coqc). *)
+
+let is_active () = not (Stack.is_empty history)
+
 (** For debug purpose, a dump of the history *)
 
 let dump_history () =
@@ -74,6 +80,14 @@ let search test =
   with Found i ->
     while i != Stack.top history do pop () done
 
+(** An auxiliary function to retrieve the number of remaining subgoals *)
+
+let get_ngoals () =
+  try
+    let prf = Proof_global.give_me_the_proof () in
+    List.length (Evd.sig_it (Proof.V82.background_subgoals prf))
+  with Proof_global.NoCurrentProof -> 0
+
 (** Register the end of a command and store the current state *)
 
 let mark_command ast =
@@ -85,6 +99,7 @@ let mark_command ast =
       prfname = (try Some (Pfedit.get_current_proof_name ()) with _ -> None);
       prfdepth = max 0 (Pfedit.current_proof_depth ());
       reachable = true;
+      ngoals = get_ngoals ();
       cmd = ast }
     history
 
@@ -175,6 +190,7 @@ let reset_initial () =
 	nproofs = 0;
 	prfname = None;
 	prfdepth = 0;
+	ngoals = 0;
 	reachable = true;
 	cmd = VernacNop }
       history
@@ -215,10 +231,10 @@ let get_script prf =
     | _ -> ()
   in
   (try Stack.iter select history with Not_found -> ());
-  (* Get rid of intermediate commands which don't grow the depth *)
+  (* Get rid of intermediate commands which don't grow the proof depth *)
   let rec filter n = function
     | [] -> []
-    | {prfdepth=d; cmd=c}::l when n < d -> c :: filter d l
+    | {prfdepth=d; cmd=c; ngoals=ng}::l when n < d -> (c,ng) :: filter d l
     | {prfdepth=d}::l -> filter d l
   in
   (* initial proof depth (after entering the lemma statement) is 1 *)
diff --git a/toplevel/backtrack.mli b/toplevel/backtrack.mli
index 3fde5b11..413ecd2e 100644
--- a/toplevel/backtrack.mli
+++ b/toplevel/backtrack.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -19,6 +19,11 @@
 
 val mark_command : Vernacexpr.vernac_expr -> unit
 
+(** Is this history stack active (i.e. nonempty) ?
+    The stack is currently inactive when compiling files (coqc). *)
+
+val is_active : unit -> bool
+
 (** The [Invalid] exception is raised when one of the following function
     tries to empty the history stack, or reach an unknown states, etc.
     The stack is preserved in these cases. *)
@@ -76,7 +81,7 @@ val mark_unreachable : ?after:int -> Names.identifier list -> unit
 
 (** Parse the history stack for printing the script of a proof *)
 
-val get_script : Names.identifier -> Vernacexpr.vernac_expr list
+val get_script : Names.identifier -> (Vernacexpr.vernac_expr * int) list
 
 
 (** For debug purpose, a dump of the history *)
@@ -86,6 +91,7 @@ type info = {
   nproofs : int;
   prfname : Names.identifier option;
   prfdepth : int;
+  ngoals : int;
   cmd : Vernacexpr.vernac_expr;
   mutable reachable : bool;
 }
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 5f2c3dbb..3b6f0f7c 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index da9d3590..96c73eb6 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index c328cc91..52d507a1 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 2cc8c453..2228143b 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 18f12582..6914b8f0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 68a93a74..a61f4f65 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index dfb1a1b5..8bbe9454 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -294,17 +294,14 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     mind_entry_inds = entries },
     impls
 
-let eq_constr_expr c1 c2 =
-  try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
-
 (* Very syntactical equality *)
 let eq_local_binder d1 d2 = match d1,d2 with
   | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) ->
       List.length nal1 = List.length nal2 && k1 = k2 &&
       List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
-      eq_constr_expr c1 c2
+      Constrextern.is_same_type c1 c2
   | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
-      id1 = id2 && eq_constr_expr c1 c2
+      id1 = id2 && Constrextern.is_same_type c1 c2
   | _ ->
       false
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8ffdbdec..b1cf2053 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e4cfcb3f..66a9516a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -135,3 +135,11 @@ let init_ocaml_path () =
       [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ];
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
 	[ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
+
+let get_compat_version = function
+  | "8.3" -> Flags.V8_3
+  | "8.2" -> Flags.V8_2
+  | ("8.1" | "8.0") as s ->
+    warning ("Compatibility with version "^s^" not supported.");
+    Flags.V8_2
+  | s -> Util.error ("Unknown compatibility version \""^s^"\".")
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 43b1556d..9ca1deb4 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,3 +22,5 @@ val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
+
+val get_compat_version : string -> Flags.compat_version
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index a60e0d82..df388d1d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -119,13 +119,6 @@ let compile_files () =
 	   Vernac.compile v f)
       (List.rev !compile_list)
 
-let set_compat_version = function
-  | "8.3" -> compat_version := Some V8_3
-  | "8.2" -> compat_version := Some V8_2
-  | "8.1" -> warning "Compatibility with version 8.1 not supported."
-  | "8.0" -> warning "Compatibility with version 8.0 not supported."
-  | s -> error ("Unknown compatibility version \""^s^"\".")
-
 (*s options for the virtual machine *)
 
 let boxed_val = ref false
@@ -152,6 +145,9 @@ let warning s = msg_warning (str s)
 let ide_slave = ref false
 let filter_opts = ref false
 
+let verb_compat_ntn = ref false
+let no_compat_ntn = ref false
+
 let parse_args arglist =
   let glob_opt = ref false in
   let rec parse = function
@@ -243,9 +239,13 @@ let parse_args arglist =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-compat" :: v :: rem -> set_compat_version v; parse rem
+    | "-compat" :: v :: rem ->
+        Flags.compat_version := get_compat_version v; parse rem
     | "-compat" :: []       -> usage ()
 
+    | "-verbose-compat-notations" :: rem -> verb_compat_ntn := true; parse rem
+    | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem
+
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem ->
 	Flags.print_emacs := true; Pp.make_pp_emacs();
@@ -332,6 +332,9 @@ let init arglist =
       Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
+      (* Be careful to set these variables after the inputstate *)
+      Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
+      Syntax_def.set_compat_notations (not !no_compat_ntn);
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
         Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 16d2b874..73e21484 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index bab711ea..7d8807ea 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index f94ed6e3..8c64f3ed 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 958e3dcb..e7b5a0f2 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -388,15 +388,12 @@ let explain_unsolvability = function
       strbrk " (several distinct possible instances found)"
 
 let explain_typeclass_resolution env evi k =
-  match k with
-  | GoalEvar | InternalHole | ImplicitArg _ ->
-      (match Typeclasses.class_of_constr evi.evar_concl with
-      | Some c ->
-	  let env = Evd.evar_env evi in
-	    fnl () ++ str "Could not find an instance for " ++
-	      pr_lconstr_env env evi.evar_concl ++
-	      pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
-      | None -> mt())
+  match Typeclasses.class_of_constr evi.evar_concl with
+  | Some c ->
+    let env = Evd.evar_env evi in
+      fnl () ++ str "Could not find an instance for " ++
+      pr_lconstr_env env evi.evar_concl ++
+      pr_ne_context_of (str " in environment:"++ fnl ()) (str ".") env
   | _ -> mt()
 
 let explain_unsolvable_implicit env evi k explain =
@@ -698,12 +695,8 @@ let explain_no_instance env (_,id) l =
 let is_goal_evar evi = match evi.evar_source with (_, GoalEvar) -> true | _ -> false
 
 let pr_constraints printenv env evm =
-  let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evm) in
-  let evm = fold_undefined 
-    (fun ev evi evm' -> 
-       if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
-  in
   let l = Evd.to_list evm in
+  assert(l <> []);
   let (ev, evi) = List.hd l in
     if List.for_all (fun (ev', evi') ->
       eq_named_context_val evi.evar_hyps evi'.evar_hyps) l
@@ -719,18 +712,23 @@ let pr_constraints printenv env evm =
       pr_evar_map None evm
 
 let explain_unsatisfiable_constraints env evd constr =
-  let evm = Evarutil.nf_evar_map evd in
-  let undef = Evd.undefined_evars evm in
+  let evm = Evd.undefined_evars (Evarutil.nf_evar_map_undefined evd) in
+  (* Remove goal evars *)
+  let undef = fold_undefined 
+    (fun ev evi evm' -> 
+       if is_goal_evar evi then Evd.remove evm' ev else evm') evm evm
+  in
   match constr with
   | None ->
       str"Unable to satisfy the following constraints:" ++ fnl() ++
 	pr_constraints true env undef
   | Some (ev, k) ->
-      explain_unsolvable_implicit env (Evd.find evm ev) k None ++ fnl () ++
-	if List.length (Evd.to_list undef) > 1 then
-	  str"With the following constraints:" ++ fnl() ++
-	    pr_constraints false env (Evd.remove undef ev)
-	else mt ()
+      explain_typeclass_resolution env (Evd.find evm ev) k ++ fnl () ++
+	(let remaining = Evd.remove undef ev in
+	   if Evd.has_undefined remaining then
+	     str"With the following constraints:" ++ fnl() ++
+	       pr_constraints false env remaining
+	   else mt ())
 
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
@@ -995,6 +993,11 @@ let explain_reduction_tactic_error = function
 let explain_ltac_call_trace (nrep,last,trace,loc) =
   let calls =
     (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace) in
+  let tacexpr_differ te te' =
+    (* NB: The following comparison may raise an exception
+       since a tacexpr may embed a functional part via a TacExtend *)
+    try te <> te' with Invalid_argument _ -> false
+  in
   let pr_call (n,ck) =
     (match ck with
        | Proof_type.LtacNotationCall s -> quote (str s)
@@ -1006,11 +1009,11 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
 	   (Pptactic.pr_glob_tactic (Global.env())
 	      (Tacexpr.TacAtom (dummy_loc,te)))
 	   ++ (match !otac with
-		 | Some te' when (Obj.magic te' <> te) ->
-		     strbrk " (expanded to " ++ quote
-		       (Pptactic.pr_tactic (Global.env())
-			  (Tacexpr.TacAtom (dummy_loc,te')))
-		     ++ str ")"
+		 | Some te' when tacexpr_differ (Obj.magic te') te ->
+		   strbrk " (expanded to " ++ quote
+		     (Pptactic.pr_tactic (Global.env())
+			(Tacexpr.TacAtom (dummy_loc,te')))
+		   ++ str ")"
 		 | _ -> mt ())
        | Proof_type.LtacConstrInterp (c,(vars,unboundvars)) ->
 	   let filter =
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index a763472b..84d3ec95 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/ide_intf.ml b/toplevel/ide_intf.ml
index 9ba3d8b4..0df24c7a 100644
--- a/toplevel/ide_intf.ml
+++ b/toplevel/ide_intf.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@
 
 (** WARNING: TO BE UPDATED WHEN MODIFIED! *)
 
-let protocol_version = "20120511"
+let protocol_version = "20120710"
 
 (** * Interface of calls to Coq by CoqIde *)
 
@@ -338,13 +338,25 @@ let to_call = function
 
 let of_status s =
   let of_so = of_option of_string in
-  Element ("status", [], [of_so s.status_path; of_so s.status_proofname])
+  let of_sl = of_list of_string in
+  Element ("status", [],
+    [
+      of_sl s.status_path;
+      of_so s.status_proofname;
+      of_sl s.status_allproofs;
+      of_int s.status_statenum;
+      of_int s.status_proofnum;
+    ]
+  )
 
 let to_status = function
-| Element ("status", [], [path; name]) ->
+| Element ("status", [], [path; name; prfs; snum; pnum]) ->
   {
-    status_path = to_option to_string path;
+    status_path = to_list to_string path;
     status_proofname = to_option to_string name;
+    status_allproofs = to_list to_string prfs;
+    status_statenum = to_int snum;
+    status_proofnum = to_int pnum;
   }
 | _ -> raise Marshal_error
 
@@ -370,14 +382,16 @@ let to_goal = function
 | _ -> raise Marshal_error
 
 let of_goals g =
+  let of_glist = of_list of_goal in
   let fg = of_list of_goal g.fg_goals in
-  let bg = of_list of_goal g.bg_goals in
+  let bg = of_list (of_pair of_glist of_glist) g.bg_goals in
   Element ("goals", [], [fg; bg])
 
 let to_goals = function
 | Element ("goals", [], [fg; bg]) ->
+  let to_glist = to_list to_goal in
   let fg = to_list to_goal fg in
-  let bg = to_list to_goal bg in
+  let bg = to_list (to_pair to_glist to_glist) bg in
   { fg_goals = fg; bg_goals = bg; }
 | _ -> raise Marshal_error
 
@@ -495,9 +509,9 @@ let pr_string s = "["^s^"]"
 let pr_bool b = if b then "true" else "false"
 
 let pr_status s =
-  let path = match s.status_path with
-  | None -> "no path; "
-  | Some p -> "path = " ^ p ^ "; "
+  let path =
+    let l = String.concat "." s.status_path in
+    "path=" ^ l ^ ";"
   in
   let name = match s.status_proofname with
   | None -> "no proof;"
@@ -512,7 +526,14 @@ let pr_mkcases l =
 let pr_goals_aux g =
   if g.fg_goals = [] then
     if g.bg_goals = [] then "Proof completed."
-    else Printf.sprintf "Still %i unfocused goals." (List.length g.bg_goals)
+    else
+      let rec pr_focus _ = function
+      | [] -> assert false
+      | [lg, rg] -> Printf.sprintf "%i" (List.length lg + List.length rg)
+      | (lg, rg) :: l ->
+        Printf.sprintf "%i:%a" (List.length lg + List.length rg) pr_focus l
+      in
+      Printf.sprintf "Still focussed: [%a]." pr_focus g.bg_goals
   else
     let pr_menu s = s in
     let pr_goal { goal_hyp = hyps; goal_ccl = goal } =
diff --git a/toplevel/ide_intf.mli b/toplevel/ide_intf.mli
index deee50e5..26c6b671 100644
--- a/toplevel/ide_intf.mli
+++ b/toplevel/ide_intf.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/ide_slave.ml b/toplevel/ide_slave.ml
index 93ad052c..681eec0d 100644
--- a/toplevel/ide_slave.ml
+++ b/toplevel/ide_slave.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -132,13 +132,13 @@ let hyp_next_tac sigma env (id,_,ast) =
     ("exact "^id_s),("exact "^id_s^".\n");
     ("generalize "^id_s),("generalize "^id_s^".\n");
     ("absurd <"^id_s^">"),("absurd "^type_s^".\n")
-  ] @ (if Hipattern.is_equality_type ast then [
+  ] @ [
     ("discriminate "^id_s),("discriminate "^id_s^".\n");
     ("injection "^id_s),("injection "^id_s^".\n")
-  ] else []) @ (if Hipattern.is_equality_type (snd (Reductionops.splay_prod env sigma ast)) then [
+  ] @ [
     ("rewrite "^id_s),("rewrite "^id_s^".\n");
     ("rewrite <- "^id_s),("rewrite <- "^id_s^".\n")
-  ] else []) @ [
+  ] @ [
     ("elim "^id_s), ("elim "^id_s^".\n");
     ("inversion "^id_s), ("inversion "^id_s^".\n");
     ("inversion clear "^id_s), ("inversion_clear "^id_s^".\n")
@@ -150,11 +150,11 @@ let concl_next_tac sigma concl =
     "intro";
     "intros";
     "intuition"
-  ] @ (if Hipattern.is_equality_type (Goal.V82.concl sigma concl) then [
+  ] @ [
     "reflexivity";
     "discriminate";
     "symmetry"
-  ] else []) @ [
+  ] @ [
     "assumption";
     "omega";
     "ring";
@@ -180,19 +180,21 @@ let process_goal sigma g =
   let process_hyp h_env d acc =
     let d = Term.map_named_declaration (Reductionops.nf_evar sigma) d in
     (string_of_ppcmds (pr_var_decl h_env d)) :: acc in
-(*           (string_of_ppcmds (pr_var_decl h_env d), hyp_next_tac sigma h_env d)::acc in *)
   let hyps =
     List.rev (Environ.fold_named_context process_hyp env ~init: []) in
   { Interface.goal_hyp = hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; }
-(*         hyps,(ccl,concl_next_tac sigma g)) *)
 
 let goals () =
   try
     let pfts = Proof_global.give_me_the_proof () in
-    let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in
-    let fg = List.map (process_goal sigma) all_goals in
-    let { Evd.it = bgoals ; sigma = sigma } = Proof.V82.background_subgoals pfts in
-    let bg = List.map (process_goal sigma) bgoals in
+    let (goals, zipper, sigma) = Proof.proof pfts in
+    let fg = List.map (process_goal sigma) goals in
+    let map_zip (lg, rg) =
+      let lg = List.map (process_goal sigma) lg in
+      let rg = List.map (process_goal sigma) rg in
+      (lg, rg)
+    in
+    let bg = List.map map_zip zipper in
     Some { Interface.fg_goals = fg; Interface.bg_goals = bg; }
   with Proof_global.NoCurrentProof -> None
 
@@ -231,16 +233,23 @@ let status () =
       and display the other parts (opened sections and modules) *)
   let path =
     let l = Names.repr_dirpath (Lib.cwd ()) in
-    let l = snd (Util.list_sep_last l) in
-    if l = [] then None
-    else Some (Names.string_of_dirpath (Names.make_dirpath l))
+    List.rev_map Names.string_of_id l
   in
   let proof =
-    try
-      Some (Names.string_of_id (Pfedit.get_current_proof_name ()))
+    try Some (Names.string_of_id (Proof_global.get_current_proof_name ()))
     with _ -> None
   in
-  { Interface.status_path = path; Interface.status_proofname = proof }
+  let allproofs =
+    let l = Proof_global.get_all_proof_names () in
+    List.map Names.string_of_id l
+  in
+  {
+    Interface.status_path = path;
+    Interface.status_proofname = proof;
+    Interface.status_allproofs = allproofs;
+    Interface.status_statenum = Lib.current_command_label ();
+    Interface.status_proofnum = Pfedit.current_proof_depth ();
+  }
 
 (** This should be elsewhere... *)
 let search flags =
diff --git a/toplevel/ide_slave.mli b/toplevel/ide_slave.mli
index 13dff280..fb927cf3 100644
--- a/toplevel/ide_slave.mli
+++ b/toplevel/ide_slave.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index de3b62f8..9f1a0218 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 96096d47..7032eb46 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 51eddbae..fa6885af 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 87aedc7b..8ce27708 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/interface.mli b/toplevel/interface.mli
index f3374ab4..39fb2a0e 100644
--- a/toplevel/interface.mli
+++ b/toplevel/interface.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -29,17 +29,23 @@ type evar = {
 }
 
 type status = {
-  status_path : string option;
+  status_path : string list;
   (** Module path of the current proof *)
   status_proofname : string option;
-  (** Current proof name. [None] if no proof is in progress *)
+  (** Current proof name. [None] if no focussed proof is in progress *)
+  status_allproofs : string list;
+  (** List of all pending proofs. Order is not significant *)
+  status_statenum : int;
+  (** A unique id describing the state of coqtop *)
+  status_proofnum : int;
+  (** An id describing the state of the current proof. *)
 }
 
 type goals = {
   fg_goals : goal list;
   (** List of the focussed goals *)
-  bg_goals : goal list;
-  (** List of the background goals *)
+  bg_goals : (goal list * goal list) list;
+  (** Zipper representing the unfocussed background goals *)
 }
 
 type hint = (string * string) list
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 7704449f..d6ab44c6 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 8b496f82..e48cb210 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 2f98962c..5977591c 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
index a6a95ccf..cec3597a 100644
--- a/toplevel/libtypes.mli
+++ b/toplevel/libtypes.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index cdeff601..775a3af4 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -757,7 +757,7 @@ let interp_modifiers modl =
     | SetAssoc a :: l ->
 	if assoc <> None then error"An associativity is given more than once.";
 	interp (Some a) level etyps format l
-    | SetOnlyParsing :: l ->
+    | SetOnlyParsing _ :: l ->
 	onlyparsing := true;
 	interp assoc level etyps format l
     | SetFormat s :: l ->
@@ -770,8 +770,13 @@ let check_infix_modifiers modifiers =
   if t <> [] then
     error "Explicit entry level or type unexpected in infix notation."
 
-let no_syntax_modifiers modifiers =
-  modifiers = [] or modifiers = [SetOnlyParsing]
+let no_syntax_modifiers = function
+  | [] | [SetOnlyParsing _] -> true
+  | _ -> false
+
+let is_only_parsing = function
+  | [SetOnlyParsing _] -> true
+  | _ -> false
 
 (* Compute precedences from modifiers (or find default ones) *)
 
@@ -1118,7 +1123,7 @@ let add_notation local c ((loc,df),modifiers) sc =
   let df' =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
-    let onlyparse = modifiers=[SetOnlyParsing] in
+    let onlyparse = is_only_parsing modifiers in
     try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
@@ -1193,6 +1198,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       let vars,pat = interp_aconstr i_vars [] c in
       List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
   in
-  let onlyparse = onlyparse or is_not_printable pat in
+  let onlyparse = match onlyparse with
+    | None when (is_not_printable pat) -> Some Flags.Current
+    | p -> p
+  in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 32568854..38a0ae59 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -54,7 +54,7 @@ val add_syntax_extension :
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : identifier -> identifier list * constr_expr ->
-  bool -> bool -> unit
+  bool -> Flags.compat_version option -> unit
 
 (** Print the Camlp4 state of a grammar *)
 
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 025c972f..2059ca60 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -221,11 +221,6 @@ let file_of_name name =
  * (linked or loaded with load_object). It is used not to load a
  * module twice. It is NOT the list of ML modules Coq knows. *)
 
-type ml_module_object = {
-  mlocal : Vernacexpr.locality_flag;
-  mnames : string list
-}
-
 let known_loaded_modules = ref Stringset.empty
 
 let add_known_module mname =
@@ -235,8 +230,20 @@ let add_known_module mname =
 let module_is_known mname =
   Stringset.mem (String.capitalize mname) !known_loaded_modules
 
+(** A plugin is just an ML module with an initialization function. *)
+
 let known_loaded_plugins = ref Stringmap.empty
 
+let add_known_plugin init name =
+  let name = String.capitalize name in
+  add_known_module name;
+  known_loaded_plugins := Stringmap.add name init !known_loaded_plugins
+
+let init_known_plugins () =
+  Stringmap.iter (fun _ f -> f()) !known_loaded_plugins
+
+(** ml object = ml module or plugin *)
+
 let init_ml_object mname =
   try Stringmap.find mname !known_loaded_plugins ()
   with Not_found -> ()
@@ -246,81 +253,75 @@ let load_ml_object mname fname=
   add_known_module mname;
   init_ml_object mname
 
-let add_known_plugin init name =
-  let name = String.capitalize name in
-  add_known_module name;
-  known_loaded_plugins := Stringmap.add name init !known_loaded_plugins
-
-let init_known_plugins () =
-  Stringmap.iter (fun _ f -> f()) !known_loaded_plugins
-
 (* Summary of declared ML Modules *)
 
-(* List and not Stringset because order is important *)
+(* List and not Stringset because order is important: most recent first. *)
+
 let loaded_modules = ref []
-let get_loaded_modules () = !loaded_modules
+let get_loaded_modules () = List.rev !loaded_modules
 let add_loaded_module md = loaded_modules := md :: !loaded_modules
+let reset_loaded_modules () = loaded_modules := []
 
-let orig_loaded_modules = ref !loaded_modules
-let init_ml_modules () = loaded_modules := !orig_loaded_modules
+let if_verbose_load verb f name fname =
+  if not verb then f name fname
+  else
+    let info = "[Loading ML file "^fname^" ..." in
+    try
+      f name fname;
+      msgnl (str (info^" done]"));
+    with e ->
+      msgnl (str (info^" failed]"));
+      raise e
+
+(** Load a module for the first time (i.e. dynlink it)
+    or simulate its reload (i.e. doing nothing except maybe
+    an initialization function). *)
+
+let cache_ml_object verb reinit name =
+  begin
+    if module_is_known name then
+      (if reinit then init_ml_object name)
+    else if not has_dynlink then
+      error ("Dynamic link not supported (module "^name^")")
+    else
+      if_verbose_load (verb && is_verbose ())
+	load_ml_object name (file_of_name name)
+  end;
+  add_loaded_module name
 
 let unfreeze_ml_modules x =
-  loaded_modules := [];
-  List.iter
-    (fun name ->
-       let mname = mod_of_name name in
-       if not (module_is_known mname) then
-         if has_dynlink then
-           let fname = file_of_name mname in
-           load_ml_object mname fname
-         else
-	   errorlabstrm "Mltop.unfreeze_ml_modules"
-             (str"Loading of ML object file forbidden in a native Coq.")
-       else init_ml_object mname;
-       add_loaded_module mname)
-    x
+  reset_loaded_modules ();
+  List.iter (cache_ml_object false false) x
 
 let _ =
   Summary.declare_summary "ML-MODULES"
-    { Summary.freeze_function = (fun () -> List.rev (get_loaded_modules()));
-      Summary.unfreeze_function = (fun x -> unfreeze_ml_modules x);
-      Summary.init_function = (fun () -> init_ml_modules ()) }
-
-(* Same as restore_ml_modules, but verbosely *)
-
-let cache_ml_module_object (_,{mnames=mnames}) =
-  List.iter
-    (fun name ->
-       let mname = mod_of_name name in
-       if not (module_is_known mname) then
-	 if has_dynlink then
-           let fname = file_of_name mname in
-	   try
-	     if_verbose
-	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
-             load_ml_object mname fname;
-             if_verbose msgnl (str" done]");
-             add_loaded_module mname
-           with e ->
-	     if_verbose msgnl (str" failed]");
-	     raise e
-	 else
-	     (if_verbose msgnl (str" failed]");
-	      error ("Dynamic link not supported (module "^name^")"))
-       else init_ml_object mname)
-    mnames
-
-let classify_ml_module_object ({mlocal=mlocal} as o) =
+    { Summary.freeze_function = get_loaded_modules;
+      Summary.unfreeze_function = unfreeze_ml_modules;
+      Summary.init_function = reset_loaded_modules }
+
+(* Liboject entries of declared ML Modules *)
+
+type ml_module_object = {
+  mlocal : Vernacexpr.locality_flag;
+  mnames : string list
+}
+
+let cache_ml_objects (_,{mnames=mnames}) =
+  List.iter (cache_ml_object true true) mnames
+
+let classify_ml_objects ({mlocal=mlocal} as o) =
   if mlocal then Dispose else Substitute o
 
 let inMLModule : ml_module_object -> obj =
-  declare_object {(default_object "ML-MODULE") with
-                    load_function = (fun _ -> cache_ml_module_object);
-                    cache_function = cache_ml_module_object;
-                    subst_function = (fun (_,o) -> o);
-                    classify_function = classify_ml_module_object }
+  declare_object
+    {(default_object "ML-MODULE") with
+      load_function = (fun _ -> cache_ml_objects);
+      cache_function = cache_ml_objects;
+      subst_function = (fun (_,o) -> o);
+      classify_function = classify_ml_objects }
 
 let declare_ml_modules local l =
+  let l = List.map mod_of_name l in
   Lib.add_anonymous_leaf (inMLModule {mlocal=local; mnames=l})
 
 let print_ml_path () =
@@ -328,7 +329,7 @@ let print_ml_path () =
   ppnl (str"ML Load Path:" ++ fnl () ++ str"  " ++
           hv 0 (prlist_with_sep pr_fnl pr_str l))
 
-	  (* Printing of loaded ML modules *)
+(* Printing of loaded ML modules *)
 
 let print_ml_modules () =
   let l = get_loaded_modules () in
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 99b96ed7..ebea73f1 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -51,27 +51,16 @@ val add_known_module : string -> unit
 val module_is_known : string -> bool
 val load_ml_object : string -> string -> unit
 
-(* Declare a plugin and its initialization function. 
- * A plugin is just an ML module with an initialization function.
- * Adding a known plugin implies adding it as a known ML module.
- * The initialization function is granted to be called after Coq is fully
- * bootstrapped, even if the plugin is statically linked with the toplevel *)
+(** Declare a plugin and its initialization function.
+    A plugin is just an ML module with an initialization function.
+    Adding a known plugin implies adding it as a known ML module.
+    The initialization function is granted to be called after Coq is fully
+    bootstrapped, even if the plugin is statically linked with the toplevel *)
 val add_known_plugin : (unit -> unit) -> string -> unit
 
-(* Calls all initialization functions in a non-specified order *)
+(** Calls all initialization functions in a non-specified order *)
 val init_known_plugins : unit -> unit
 
-(** Summary of Declared ML Modules *)
-val get_loaded_modules : unit -> string list
-val add_loaded_module : string -> unit
-val init_ml_modules : unit -> unit
-val unfreeze_ml_modules : string list -> unit
-
-type ml_module_object = {
-  mlocal: Vernacexpr.locality_flag;
-  mnames: string list;
-}
-
 val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit
 
 val print_ml_path : unit -> unit
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 0c55861f..3708c2f7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 45670f1f..f4ae7832 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 33e8e51d..3e182689 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/search.mli b/toplevel/search.mli
index 95827d54..76821e62 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 8514872b..d5321623 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 757aab1a..0af05d02 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8c9b1078..f6505e30 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -32,6 +32,8 @@ let print_usage_channel co command =
 \n  -nois                  start with an empty state\
 \n  -outputstate f         write state in file f.coq\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
+\n  -verbose-compat-notations  be warned when using compatibility notations\
+\n  -no-compat-notations   get an error when using compatibility notations\
 \n\
 \n  -load-ml-object f      load ML object file f\
 \n  -load-ml-source f      load ML file f\
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 0b98f061..45cedf44 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index ed20fc60..3314e82c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -26,6 +26,30 @@ exception DuringCommandInterp of Util.loc * exn
 
 exception HasNotFailed
 
+(* When doing Load on a file, two behaviors are possible:
+
+   - either the history stack is grown by only one command,
+     the "Load" itself. This is mandatory for command-counting
+     interfaces (CoqIDE).
+
+   - either each individual sub-commands in the file is added
+     to the history stack. This allows commands like Show Script
+     to work across the loaded file boundary (cf. bug #2820).
+
+   The best of the two could probably be combined someday,
+   in the meanwhile we use a flag. *)
+
+let atomic_load = ref true
+
+let _ =
+  Goptions.declare_bool_option
+    { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
+      Goptions.optname  = "atomic registration of commands in a Load";
+      Goptions.optkey   = ["Atomic";"Load"];
+      Goptions.optread  = (fun () -> !atomic_load);
+      Goptions.optwrite = ((:=) atomic_load) }
+
 (* Specifies which file is read. The intermediate file names are
    discarded here. The Drop exception becomes an error. We forget
    if the error ocurred during interpretation or not *)
@@ -272,16 +296,24 @@ and read_vernac_file verbosely s =
     else Flags.silently Vernacentries.interp
   in
   let checknav loc cmd =
-    if is_navigation_vernac cmd then
+    if is_navigation_vernac cmd && not (is_reset cmd) then
 	user_error loc "Navigation commands forbidden in files"
   in
+  let end_inner_command cmd =
+    if !atomic_load || is_reset cmd then
+      Lib.mark_end_of_command () (* for Reset in coqc or coqtop -l *)
+    else
+      Backtrack.mark_command cmd; (* for Show Script, cf bug #2820 *)
+  in
   let (in_chan, fname, input) =
     open_file_twice_if verbosely s in
   try
     (* we go out of the following infinite loop when a End_of_input is
      * raised, which means that we raised the end of the file being loaded *)
     while true do
-      vernac_com interpfun checknav (parse_sentence input);
+      let loc_ast = parse_sentence input in
+      vernac_com interpfun checknav loc_ast;
+      end_inner_command (snd loc_ast);
       pp_flush ()
     done
   with e ->   (* whatever the exception *)
@@ -324,6 +356,7 @@ let load_vernac verb file =
   chan_beautify :=
     if !Flags.beautify_file then open_out (file^beautify_suffix) else stdout;
   try
+    Lib.mark_end_of_command (); (* in case we're still in coqtop init *)
     read_vernac_file verb file;
     if !Flags.beautify_file then close_out !chan_beautify;
   with e ->
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index bcfe9b71..96bc8865 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2324e3e9..fe6bf7db 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -72,10 +72,59 @@ let show_node () =
       could, possibly, be cleaned away. (Feb. 2010) *)
   ()
 
+(* indentation code for Show Script, initially contributed
+   by D. de Rauglaudre *)
+
+let indent_script_item ((ng1,ngl1),nl,beginend,ppl) (cmd,ng) =
+  (* ng1 : number of goals remaining at the current level (before cmd)
+     ngl1 : stack of previous levels with their remaining goals
+     ng : number of goals after the execution of cmd
+     beginend : special indentation stack for { } *)
+  let ngprev = List.fold_left (+) ng1 ngl1 in
+  let new_ngl =
+    if ng > ngprev then
+      (* We've branched *)
+      (ng - ngprev + 1, ng1 - 1 :: ngl1)
+    else if ng < ngprev then
+      (* A subgoal have been solved. Let's compute the new current level
+	 by discarding all levels with 0 remaining goals. *)
+      let _ = assert (ng = ngprev - 1) in
+      let rec loop = function
+	| (0, ng2::ngl2) -> loop (ng2,ngl2)
+	| p -> p
+      in loop (ng1-1, ngl1)
+    else
+      (* Standard case, same goal number as before *)
+      (ng1, ngl1)
+  in
+  (* When a subgoal have been solved, separate this block by an empty line *)
+  let new_nl = (ng < ngprev)
+  in
+  (* Indentation depth *)
+  let ind = List.length ngl1
+  in
+  (* Some special handling of bullets and { }, to get a nicer display *)
+  let pred n = max 0 (n-1) in
+  let ind, nl, new_beginend = match cmd with
+    | VernacSubproof _ -> pred ind, nl, (pred ind)::beginend
+    | VernacEndSubproof -> List.hd beginend, false, List.tl beginend
+    | VernacBullet _ -> pred ind, nl, beginend
+    | _ -> ind, nl, beginend
+  in
+  let pp =
+    (if nl then fnl () else mt ()) ++
+    (hov (ind+1) (str (String.make ind ' ') ++ Ppvernac.pr_vernac cmd))
+  in
+  (new_ngl, new_nl, new_beginend, pp :: ppl)
+
 let show_script () =
   let prf = Pfedit.get_current_proof_name () in
   let cmds = Backtrack.get_script prf in
-  msgnl (Util.prlist_with_sep Pp.fnl Ppvernac.pr_vernac cmds)
+  let _,_,_,indented_cmds =
+    List.fold_left indent_script_item ((1,[]),false,[],[]) cmds
+  in
+  let indented_cmds = List.rev (indented_cmds) in
+  msgnl (v 0 (Util.prlist_with_sep Pp.fnl (fun x -> x) indented_cmds))
 
 let show_thesis () =
      msgnl (anomaly "TODO" )
@@ -311,6 +360,11 @@ let smart_global r =
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
     gr
 
+let dump_global r =
+  try
+    let gr = Smartlocate.smart_global r in
+    Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr
+  with _ -> ()
 (**********)
 (* Syntax *)
 
@@ -389,8 +443,10 @@ let vernac_end_proof = function
 let vernac_exact_proof c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the begining of a proof. *)
-    by (Tactics.exact_proof c);
-      save_named true
+  let prf = Pfedit.get_current_proof_name () in
+  by (Tactics.exact_proof c);
+  save_named true;
+  Backtrack.mark_unreachable [prf]
 
 let vernac_assumption kind l nl=
   let global = fst kind = Global in
@@ -458,9 +514,21 @@ let vernac_cofixpoint l =
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
   do_cofixpoint l
 
-let vernac_scheme = Indschemes.do_scheme
-
-let vernac_combined_scheme = Indschemes.do_combined_scheme
+let vernac_scheme l =
+  if Dumpglob.dump () then
+    List.iter (fun (lid, s) ->
+	       Option.iter (fun lid -> Dumpglob.dump_definition lid false "def") lid;
+	       match s with
+	       | InductionScheme (_, r, _)
+	       | CaseScheme (_, r, _) 
+	       | EqualityScheme r -> dump_global r) l;
+  Indschemes.do_scheme l
+
+let vernac_combined_scheme lid l =
+  if Dumpglob.dump () then
+    (Dumpglob.dump_definition lid false "def";
+     List.iter (fun lid -> dump_global (Genarg.AN (Ident lid))) l);
+ Indschemes.do_combined_scheme lid l
 
 (**********************)
 (* Modules            *)
@@ -1190,6 +1258,7 @@ let vernac_check_may_eval redexp glopt rc =
 	if !pcoq <> None then (Option.get !pcoq).print_check env j
 	else msg (print_judgment env j)
     | Some r ->
+        Tacinterp.dump_glob_red_expr r;
         let (sigma',r_interp) = interp_redexp env sigma' r in
 	let redfun = fst (reduction_of_red_expr r_interp) in
 	if !pcoq <> None
@@ -1248,8 +1317,10 @@ let vernac_print = function
       pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
       pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
-  | PrintAbout qid -> msg (print_about qid)
-  | PrintImplicit qid -> msg (print_impargs qid)
+  | PrintAbout qid -> 
+    msg (print_about qid)
+  | PrintImplicit qid -> 
+    dump_global qid; msg (print_impargs qid)
   | PrintAssumptions (o,r) ->
       (* Prints all the axioms and section variables used by a term *)
       let cstr = constr_of_global (smart_global r) in
@@ -1340,10 +1411,43 @@ let vernac_back n =
   with Backtrack.Invalid -> error "Invalid backtrack."
 
 let vernac_reset_name id =
-  try Backtrack.reset_name id; try_print_subgoals ()
-  with Backtrack.Invalid -> error "Invalid Reset."
+  try
+    let globalized =
+      try
+	let gr = Smartlocate.global_with_alias (Ident id) in
+	Dumpglob.add_glob (fst id) gr;
+	true
+      with _ -> false in
+
+    if not globalized then begin
+       try begin match Lib.find_opening_node (snd id) with
+          | Lib.OpenedSection _ -> Dumpglob.dump_reference (fst id)
+              (string_of_dirpath (Lib.current_dirpath true)) "<>" "sec";
+          (* Might be nice to implement module cases, too.... *)
+          | _ -> ()
+       end with UserError _ -> ()
+    end;
 
-let vernac_reset_initial () = Backtrack.reset_initial ()
+    if Backtrack.is_active () then
+      (Backtrack.reset_name id; try_print_subgoals ())
+    else
+      (* When compiling files, Reset is now allowed again
+	 as asked by A. Chlipala. we emulate a simple reset,
+	 that discards all proofs. *)
+      let lbl = Lib.label_before_name id in
+      Pfedit.delete_all_proofs ();
+      Pp.msg_warning (str "Reset command occurred in non-interactive mode.");
+      Lib.reset_label lbl
+  with Backtrack.Invalid | Not_found -> error "Invalid Reset."
+
+
+let vernac_reset_initial () =
+  if Backtrack.is_active () then
+    Backtrack.reset_initial ()
+  else begin
+    Pp.msg_warning (str "Reset command occurred in non-interactive mode.");
+    Lib.reset_label Lib.first_command_label
+  end
 
 (* For compatibility with ProofGeneral: *)
 
@@ -1393,7 +1497,10 @@ let vernac_undoto n =
 let vernac_focus gln =
   let p = Proof_global.give_me_the_proof () in
   let n = match gln with None -> 1 | Some n -> n in
-  Proof.focus focus_command_cond () n p; print_subgoals ()
+  if n = 0 then
+    Util.error "Invalid goal number: 0. Goal numbering starts with 1."
+  else
+    Proof.focus focus_command_cond () n p; print_subgoals ()
 
   (* Unfocuses one step in the focus stack. *)
 let vernac_unfocus () =
@@ -1594,11 +1701,11 @@ let interp c = match c with
   | VernacEndSubproof -> vernac_end_subproof ()
   | VernacShow s -> vernac_show s
   | VernacCheckGuard -> vernac_check_guard ()
-  | VernacProof (None, None) -> ()
-  | VernacProof (Some tac, None) -> vernac_set_end_tac tac
-  | VernacProof (None, Some l) -> vernac_set_used_variables l
+  | VernacProof (None, None) -> print_subgoals ()
+  | VernacProof (Some tac, None) -> vernac_set_end_tac tac ; print_subgoals ()
+  | VernacProof (None, Some l) -> vernac_set_used_variables l ; print_subgoals ()
   | VernacProof (Some tac, Some l) -> 
-      vernac_set_end_tac tac; vernac_set_used_variables l
+      vernac_set_end_tac tac; vernac_set_used_variables l ; print_subgoals ()
   | VernacProofMode mn -> Proof_global.set_proof_mode mn
   (* Toplevel control *)
   | VernacToplevelControl e -> raise e
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index a9d384ea..b0d41b15 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,6 +12,8 @@ open Vernacinterp
 open Vernacexpr
 open Topconstr
 
+val dump_global : Libnames.reference Genarg.or_by_notation -> unit
+
 (** Vernacular entries *)
 
 val show_script : unit -> unit
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d9f15337..3106e866 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -128,9 +128,12 @@ type instance_flag  = bool option (* Some true = Backward instance; Some false =
 type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
 type inductive_flag = Decl_kinds.recursivity_kind
-type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 type full_locality_flag = bool option (* true = Local; false = Global      *)
+type onlyparsing_flag = Flags.compat_version option
+ (* Some v = Parse only;  None = Print also.
+    If v<>Current, it contains the name of the coq version
+    which this notation is trying to be compatible with *)
 
 type option_value = Goptionstyp.option_value =
   | BoolValue of bool
@@ -189,7 +192,7 @@ type syntax_modifier =
   | SetLevel of int
   | SetAssoc of gram_assoc
   | SetEntryType of string * simple_constr_prod_entry_key
-  | SetOnlyParsing
+  | SetOnlyParsing of Flags.compat_version
   | SetFormat of string located
 
 type proof_end =
@@ -377,13 +380,20 @@ let rec is_navigation_vernac = function
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
+  | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *)
   | c -> is_deep_navigation_vernac c
 
 and is_deep_navigation_vernac = function
-  | VernacTime c | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
+  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
   | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
   | _ -> false
 
+(* NB: Reset is now allowed again as asked by A. Chlipala *)
+
+let is_reset = function
+  | VernacResetInitial | VernacResetName _ -> true
+  | _ -> false
+
 (* Locating errors raised just after the dot is parsed but before the
    interpretation phase *)
 
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index 10c5a00f..c4cc4ae5 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 5fdc2b2c..efe7e073 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index aa38e9e9..f90cae73 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index b0fb5491..fed8332b 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.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-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)