Imported Upstream version 8.3upstream/8.3

10 files changed, 108 insertions, 96 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 5828f12d..db2f9ae9 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
 
 open Pp
 open Util
@@ -28,6 +28,8 @@ let guill s = "\""^s^"\""
 let where s =
   if !Flags.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
+exception EvaluatedError of std_ppcmds * exn option
+
 (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
 let rec explain_exn_default_aux anomaly_string report_fn = function
@@ -69,54 +71,6 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
   | Sys.Break ->
       hov 0 (fnl () ++ str "User interrupt.")
-  | Univ.UniverseInconsistency (o,u,v) ->
-      let msg =
-	if !Constrextern.print_universes then
-	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
-          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
-	  ++ spc() ++ Univ.pr_uni v ++ str")"
-	else
-	  mt() in
-      hov 0 (str "Error: Universe inconsistency" ++ msg ++ str ".")
-  | TypeError(ctx,te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
-  | PretypeError(ctx,te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
-  | Typeclasses_errors.TypeClassError(env, te) ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_typeclass_error env te)
-  | InductiveError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
-  | RecursionSchemeError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
-  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
-      explain_exn_default_aux anomaly_string report_fn exc
-  | Proof_type.LtacLocated (s,exc) ->
-      hov 0 (Himsg.explain_ltac_call_trace s ++ fnl ()
-             ++ explain_exn_default_aux anomaly_string report_fn exc)
-  | Cases.PatternMatchingError (env,e) ->
-      hov 0
-	(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
-  | Tacred.ReductionTacticError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
-  | Logic.RefinerError e ->
-      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
-  | Nametab.GlobalizationError q ->
-      hov 0 (str "Error:" ++ spc () ++
-	       str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
-	       spc () ++ str "was not found" ++
-	       spc () ++ str "in the current" ++ spc () ++ str "environment.")
-  | Nametab.GlobalizationConstantError q ->
-      hov 0 (str "Error:" ++ spc () ++
-	       str "No constant of this name:" ++ spc () ++
-               Libnames.pr_qualid q ++ str ".")
-  | Refiner.FailError (i,s) ->
-      hov 0 (str "Error: Tactic failure" ++
-                (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
-                if i=0 then str "." else str " (level " ++ int i ++ str").")
-  | Stdpp.Exc_located (loc,exc) ->
-      hov 0 ((if loc = dummy_loc then (mt ())
-               else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Lexer.Error Illegal_character ->
       hov 0 (str "Syntax error: Illegal character.")
   | Lexer.Error Unterminated_comment ->
@@ -140,12 +94,69 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
 	       else
 		 (mt ())) ++
 	       report_fn ())
-  | AlreadyDeclared msg ->
-      hov 0 (msg ++ str ".")
+  | EvaluatedError (msg,None) ->
+      msg
+  | EvaluatedError (msg,Some reraise) ->
+      msg ++ explain_exn_default_aux anomaly_string report_fn reraise
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise) ++ report_fn ())
 
+let wrap_vernac_error strm =
+  EvaluatedError (hov 0 (str "Error:" ++ spc () ++ strm), None)
+
+let rec process_vernac_interp_error = function
+  | Univ.UniverseInconsistency (o,u,v) ->
+      let msg =
+	if !Constrextern.print_universes then
+	  spc() ++ str "(cannot enforce" ++ spc() ++ Univ.pr_uni u ++ spc() ++
+          str (match o with Univ.Lt -> "<" | Univ.Le -> "<=" | Univ.Eq -> "=")
+	  ++ spc() ++ Univ.pr_uni v ++ str")"
+	else
+	  mt() in
+      wrap_vernac_error (str "Universe inconsistency" ++ msg ++ str ".")
+  | TypeError(ctx,te) ->
+      wrap_vernac_error (Himsg.explain_type_error ctx te)
+  | PretypeError(ctx,te) ->
+      wrap_vernac_error (Himsg.explain_pretype_error ctx te)
+  | Typeclasses_errors.TypeClassError(env, te) ->
+      wrap_vernac_error (Himsg.explain_typeclass_error env te)
+  | InductiveError e ->
+      wrap_vernac_error (Himsg.explain_inductive_error e)
+  | RecursionSchemeError e ->
+      wrap_vernac_error (Himsg.explain_recursion_scheme_error e)
+  | Cases.PatternMatchingError (env,e) ->
+      wrap_vernac_error (Himsg.explain_pattern_matching_error env e)
+  | Tacred.ReductionTacticError e ->
+      wrap_vernac_error (Himsg.explain_reduction_tactic_error e)
+  | Logic.RefinerError e ->
+      wrap_vernac_error (Himsg.explain_refiner_error e)
+  | Nametab.GlobalizationError q ->
+      wrap_vernac_error
+        (str "The reference" ++ spc () ++ Libnames.pr_qualid q ++
+	 spc () ++ str "was not found" ++
+	 spc () ++ str "in the current" ++ spc () ++ str "environment.")
+  | Nametab.GlobalizationConstantError q ->
+      wrap_vernac_error
+        (str "No constant of this name:" ++ spc () ++
+         Libnames.pr_qualid q ++ str ".")
+  | Refiner.FailError (i,s) ->
+      EvaluatedError (hov 0 (str "Error: Tactic failure" ++
+                (if Lazy.force s <> mt() then str ":" ++ Lazy.force s else mt ()) ++
+                if i=0 then str "." else str " (level " ++ int i ++ str")."),
+                None)
+  | AlreadyDeclared msg ->
+      wrap_vernac_error (msg ++ str ".")
+  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when Lazy.force s <> mt () ->
+      process_vernac_interp_error exc
+  | Proof_type.LtacLocated (s,exc) ->
+      EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
+        Some (process_vernac_interp_error exc))
+  | Stdpp.Exc_located (loc,exc) ->
+      Stdpp.Exc_located (loc,process_vernac_interp_error exc)
+  | exc ->
+      exc
+
 let anomaly_string () = str "Anomaly: "
 
 let report () = (str "." ++ spc () ++ str "Please report.")
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 00316007..31e0e04f 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cerrors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: cerrors.mli 13431 2010-09-18 08:15:29Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -19,10 +19,14 @@ val print_loc : loc -> std_ppcmds
 
 val explain_exn : exn -> std_ppcmds
 
-(** Same, but will re-raise all anomalies instead of explaining them *)
+(** Precompute errors raised during vernac interpretation *)
 
 val explain_exn_no_anomaly : exn -> std_ppcmds
 
+(** Pre-explain a vernac interpretation error *)
+
+val process_vernac_interp_error : exn -> exn
+
 (** For debugging purpose (?), the explain function can be twicked *)
 
 val explain_exn_function : (exn -> std_ppcmds) ref
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 435ddb4d..2d8aabfc 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: classes.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -233,7 +233,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
 		if rest <> [] then
 		  unbound_method env' k.cl_impl (get_id (fst (List.hd rest)))
 		else
-		  Inl (type_ctx_instance evars env' k.cl_props props subst)
+		  Inl (type_ctx_instance evars (push_rel_context ctx' env') k.cl_props props subst)
 	in	  
 	evars := Evarutil.nf_evar_map !evars;
 	let term, termtype =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a080442c..99ca9879 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: himsg.ml 13465 2010-09-24 22:23:07Z herbelin $ *)
 
 open Pp
 open Util
@@ -290,6 +290,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj =
   pr_ne_context_of (str "In environment") env ++
   st ++ str "." ++ fnl () ++
   (try (* May fail with unresolved globals. *)
+      let fixenv = make_all_name_different fixenv in
       let pvd = pr_lconstr_env fixenv vdefj.(i).uj_val in
 	str"Recursive definition is:" ++ spc () ++ pvd ++ str "."
     with _ -> mt ())
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 4e28ccac..c2d5f31d 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ind_tables.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ind_tables.ml 13392 2010-09-02 12:11:15Z vsiles $ i*)
 
 (* File created by Vincent Siles, Oct 2007, extended into a generic
    support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
@@ -125,7 +125,7 @@ let define internal id c =
 	const_entry_boxed = Flags.boxed_definitions() },
       Decl_kinds.IsDefinition Scheme) in
   (match internal with
-  | KernelSilent -> ()
+  | KernelSilent -> () 
   | _-> definition_message id);
   kn
 
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 29d7a12c..9031d8a3 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: indschemes.ml 13333 2010-07-27 10:18:30Z vsiles $ *)
+(* $Id: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *)
 
 (* Created by Hugo Herbelin from contents related to inductive schemes
    initially developed by Christine Paulin (induction schemes), Vincent
@@ -123,8 +123,8 @@ let declare_beq_scheme_gen internal names kn =
 
 let alarm what internal msg =
   let debug = false in
-  (* TODO: specify even more by distinguish KernelVerbose and UserVerbose *)
   match internal with
+  | KernelVerbose 
   | KernelSilent ->
     (if debug then
       Flags.if_verbose Pp.msg_warning
@@ -172,17 +172,15 @@ let beq_scheme_msg mind =
 let declare_beq_scheme_with l kn =
   try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserVerbose l kn
 
-(* TODO : maybe switch to KernelVerbose to have the right behaviour *)
 let try_declare_beq_scheme kn =
   (* TODO: handle Fix, see e.g. TheoryList.In_spec, eventually handle
       proof-irrelevance; improve decidability by depending on decidability
       for the parameters rather than on the bl and lb properties *)
-  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelSilent [] kn
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen KernelVerbose [] kn
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
 (* Case analysis schemes *)
-(* TODO: maybe switch to KernelVerbose *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -192,7 +190,7 @@ let declare_one_case_analysis_scheme ind =
        induction scheme, the other ones share the same code with the
        apropriate type *)
   if List.mem InType kelim then
-    ignore (define_individual_scheme dep KernelSilent None ind)
+    ignore (define_individual_scheme dep KernelVerbose None ind)
 
 (* Induction/recursion schemes *)
 
@@ -206,7 +204,6 @@ let kinds_from_type =
    InProp,ind_dep_scheme_kind_from_type;
    InSet,rec_dep_scheme_kind_from_type]
 
-  (* TODO: maybe switch to kernel verbose *)
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
@@ -216,7 +213,7 @@ let declare_one_induction_scheme ind =
     list_map_filter (fun (sort,kind) ->
       if List.mem sort kelim then Some kind else None)
       (if from_prop then kinds_from_prop else kinds_from_type) in
-  List.iter (fun kind -> ignore (define_individual_scheme kind KernelSilent None ind))
+  List.iter (fun kind -> ignore (define_individual_scheme kind KernelVerbose None ind))
     elims
 
 let declare_induction_schemes kn =
@@ -241,10 +238,9 @@ let declare_eq_decidability_scheme_with l kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
     declare_eq_decidability_gen UserVerbose l kn
 
-(* TODO:  maybe switch to kernel verbose *)
 let try_declare_eq_decidability kn =
   try_declare_scheme (eq_dec_scheme_msg (kn,0))
-    declare_eq_decidability_gen KernelSilent [] kn
+    declare_eq_decidability_gen KernelVerbose [] kn
 
 let declare_eq_decidability = declare_eq_decidability_scheme_with []
 
@@ -252,36 +248,34 @@ let ignore_error f x = try ignore (f x) with _ -> ()
 
 let declare_rewriting_schemes ind =
   if Hipattern.is_inductive_equality ind then begin
-    ignore (define_individual_scheme rew_r2l_scheme_kind KernelSilent None ind);
-    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelSilent None ind);
+    ignore (define_individual_scheme rew_r2l_scheme_kind KernelVerbose None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind KernelVerbose None ind);
     ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
-      KernelSilent None ind);
+      KernelVerbose None ind);
     (* These ones expect the equality to be symmetric; the first one also *)
     (* needs eq *)
-    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelSilent None) ind;
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind KernelVerbose None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_dep_scheme_kind KernelSilent None) ind;
+      (define_individual_scheme rew_l2r_dep_scheme_kind KernelVerbose None) ind;
     ignore_error
-      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelSilent None) ind
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind KernelVerbose None) ind
   end
 
-(* TODO: maybe switch to kernel verbose *)
 let declare_congr_scheme ind =
   if Hipattern.is_equality_type (mkInd ind) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with _ -> false
     then
-      ignore (define_individual_scheme congr_scheme_kind KernelSilent None ind)
+      ignore (define_individual_scheme congr_scheme_kind KernelVerbose None ind)
     else
       warning "Cannot build congruence scheme because eq is not found"
   end
 
-(* TODO: maybe switch to kernel verbose *)
 let declare_sym_scheme ind =
   if Hipattern.is_inductive_equality ind then
     (* Expect the equality to be symmetric *)
-    ignore_error (define_individual_scheme sym_scheme_kind KernelSilent None) ind
+    ignore_error (define_individual_scheme sym_scheme_kind KernelVerbose None) ind
 
 (* Scheme command *)
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index cd569178..773d3390 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: record.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
 
 open Pp
 open Util
@@ -259,8 +259,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_record = true;
       mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
-(* TODO : maybe switch to KernelVerbose *)
-  let kn = Command.declare_mutual_inductive_with_eliminations KernelSilent mie [(paramimpls,[])] in
+  let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
   let cstr = (rsp,1) in
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
@@ -325,8 +324,8 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	  (DefinitionEntry proj_entry, IsDefinition Definition)
 	in
 	let cref = ConstRef cst in
-	Impargs.declare_manual_implicits false cref paramimpls;
-	Impargs.declare_manual_implicits false (ConstRef proj_cst) (List.hd fieldimpls);
+	Impargs.declare_manual_implicits false cref [paramimpls];
+	Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
 	Classes.set_typeclass_transparency (EvalConstRef cst) false;
 	if infer then Evd.fold (fun ev evi _ -> Recordops.declare_method (ConstRef cst) ev sign) sign ();
 	cref, [proj_name, Some proj_cst]
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7f8bcb9e..a00efc5c 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -44,7 +44,7 @@ let raise_with_file file exc =
           ((b, f, loc), e)
       | Stdpp.Exc_located (loc, e) when loc <> dummy_loc ->
           ((false,file, loc), e)
-      | _ -> ((false,file,cmdloc), re)
+      | Stdpp.Exc_located (_, e) | e -> ((false,file,cmdloc), e)
   in
   raise (Error_in_file (file, inner, disable_drop inex))
 
@@ -198,7 +198,10 @@ let rec vernac_com interpfun (loc,com) =
 	  with e -> stop(); raise e
 	end
 
-    | v -> if not !just_parsing then interpfun v
+    | v ->
+        if not !just_parsing then
+          States.with_heavy_rollback interpfun
+            Cerrors.process_vernac_interp_error v
 
   in
     try
@@ -239,7 +242,7 @@ and read_vernac_file verbosely s =
  * backtracking. *)
 
 let raw_do_vernac po =
-  vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
+  vernac Vernacentries.interp (po,None);
   Lib.add_frozen_state();
   Lib.mark_end_of_command()
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 254f690c..d74711c2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml 13329 2010-07-26 11:05:39Z herbelin $ i*)
+(*i $Id: vernacentries.ml 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -172,7 +172,7 @@ let show_match id =
 	    | [] -> assert false
 	    | [x] -> "| "^ x  ^ " => \n" ^ acc
 	    | x::l ->
-		"| (" ^ List.fold_left (fun acc s ->  acc ^ " " ^ s) x l ^ ")"
+		"| " ^ List.fold_left (fun acc s ->  acc ^ " " ^ s) x l
 		^ " => \n" ^ acc)
 	"end" patterns in
     msg (str ("match # with\n" ^ cases))
@@ -775,11 +775,11 @@ let vernac_syntactic_definition lid =
   Metasyntax.add_syntactic_definition (snd lid)
 
 let vernac_declare_implicits local r = function
-  | Some imps ->
-      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
-	(List.map (fun (ex,b,f) -> ex, (b,true,f)) imps)
-  | None ->
+  | [] ->
       Impargs.declare_implicits local (smart_global r)
+  | _::_ as imps ->
+      Impargs.declare_manual_implicits local (smart_global r) ~enriching:false
+	(List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps)
 
 let vernac_reserve bl =
   let sb_decl = (fun (idl,c) ->
@@ -1113,7 +1113,7 @@ let vernac_print = function
       pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s)
   | PrintVisibility s ->
       pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
-  | PrintAbout qid -> msgnl (print_about qid)
+  | PrintAbout qid -> msg (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
   | PrintAssumptions (o,r) ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 5eb220cb..b5af665c 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: vernacexpr.ml 13492 2010-10-04 21:20:01Z herbelin $ i*)
 
 open Util
 open Names
@@ -313,7 +313,7 @@ type vernac_expr =
   | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
       locality_flag * onlyparsing_flag
   | VernacDeclareImplicits of locality_flag * reference or_by_notation *
-      (explicitation * bool * bool) list option
+      (explicitation * bool * bool) list list
   | VernacReserve of simple_binder list
   | VernacGeneralizable of locality_flag * (lident list) option
   | VernacSetOpacity of