Imported Upstream version 8.3pl1upstream/8.3pl1

6 files changed, 35 insertions, 35 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index db2f9ae9..3bba0605 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml 13431 2010-09-18 08:15:29Z herbelin $ *)
+(* $Id: cerrors.ml 13639 2010-11-16 15:36:01Z glondu $ *)
 
 open Pp
 open Util
@@ -81,6 +81,10 @@ let rec explain_exn_default_aux anomaly_string report_fn = function
       hov 0 (str "Syntax error: Undefined token.")
   | Lexer.Error (Bad_token s) ->
       hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ 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)
   | Assert_failure (s,b,e) ->
       hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s <> "" then
@@ -167,10 +171,13 @@ let explain_exn_default =
 let raise_if_debug e =
   if !Flags.debug then raise e
 
-let _ = Tactic_debug.explain_logic_error := explain_exn_default
+let _ = Tactic_debug.explain_logic_error :=
+  (fun e -> explain_exn_default (process_vernac_interp_error e))
 
 let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-          explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
+  (fun e ->
+    explain_exn_default_aux (fun () -> mt()) (fun () -> str ".")
+      (process_vernac_interp_error e))
 
 let explain_exn_function = ref explain_exn_default
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 9b18ef27..2d0cdea6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: command.ml 13672 2010-12-03 20:05:46Z herbelin $ *)
 
 open Pp
 open Util
@@ -241,7 +241,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
   let env_ar_params = push_rel_context ctx_params env_ar in
 
   (* Compute interpretation metadatas *)
-  let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in
+  let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (rel_context_nhyps ctx_params) impls) arities in
   let arities = List.map fst arities in
   let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -275,7 +275,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite =
     mind_entry_lc = ctypes
   }) indl arities constructors in
   let impls =
-    let len = List.length ctx_params in
+    let len = rel_context_nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6ee00f48..c1663685 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml 13329 2010-07-26 11:05:39Z herbelin $ *)
+(* $Id: metasyntax.ml 13690 2010-12-06 16:15:54Z glondu $ *)
 
 open Pp
 open Flags
@@ -106,33 +106,33 @@ let add_tactic_notation (n,prods,e) =
 let print_grammar = function
   | "constr" | "operconstr" | "binder_constr" ->
       msgnl (str "Entry constr is");
-      Gram.Entry.print Pcoq.Constr.constr;
+      entry_print Pcoq.Constr.constr;
       msgnl (str "and lconstr is");
-      Gram.Entry.print Pcoq.Constr.lconstr;
+      entry_print Pcoq.Constr.lconstr;
       msgnl (str "where binder_constr is");
-      Gram.Entry.print Pcoq.Constr.binder_constr;
+      entry_print Pcoq.Constr.binder_constr;
       msgnl (str "and operconstr is");
-      Gram.Entry.print Pcoq.Constr.operconstr;
+      entry_print Pcoq.Constr.operconstr;
   | "pattern" ->
-      Gram.Entry.print Pcoq.Constr.pattern
+      entry_print Pcoq.Constr.pattern
   | "tactic" ->
       msgnl (str "Entry tactic_expr is");
-      Gram.Entry.print Pcoq.Tactic.tactic_expr;
+      entry_print Pcoq.Tactic.tactic_expr;
       msgnl (str "Entry binder_tactic is");
-      Gram.Entry.print Pcoq.Tactic.binder_tactic;
+      entry_print Pcoq.Tactic.binder_tactic;
       msgnl (str "Entry simple_tactic is");
-      Gram.Entry.print Pcoq.Tactic.simple_tactic;
+      entry_print Pcoq.Tactic.simple_tactic;
   | "vernac" ->
       msgnl (str "Entry vernac is");
-      Gram.Entry.print Pcoq.Vernac_.vernac;
+      entry_print Pcoq.Vernac_.vernac;
       msgnl (str "Entry command is");
-      Gram.Entry.print Pcoq.Vernac_.command;
+      entry_print Pcoq.Vernac_.command;
       msgnl (str "Entry syntax is");
-      Gram.Entry.print Pcoq.Vernac_.syntax;
+      entry_print Pcoq.Vernac_.syntax;
       msgnl (str "Entry gallina is");
-      Gram.Entry.print Pcoq.Vernac_.gallina;
+      entry_print Pcoq.Vernac_.gallina;
       msgnl (str "Entry gallina_ext is");
-      Gram.Entry.print Pcoq.Vernac_.gallina_ext;
+      entry_print Pcoq.Vernac_.gallina_ext;
   | _ -> error "Unknown or unprintable grammar entry."
 
 (**********************************************************************)
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 9594c988..299214f0 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -276,7 +276,6 @@ let rec is_pervasive_exn = function
   | Error_in_file (_,_,e) -> is_pervasive_exn e
   | Stdpp.Exc_located (_,e) -> is_pervasive_exn e
   | DuringCommandInterp (_,e) -> is_pervasive_exn e
-  | DuringSyntaxChecking (_,e) -> is_pervasive_exn e
   | _ -> false
 
 (* Toplevel error explanation, dealing with locations, Drop, Ctrl-D
@@ -285,8 +284,7 @@ let rec is_pervasive_exn = function
 let print_toplevel_error exc =
   let (dloc,exc) =
     match exc with
-      | DuringCommandInterp (loc,ie)
-      | DuringSyntaxChecking (loc,ie) ->
+      | DuringCommandInterp (loc,ie) ->
           if loc = dummy_loc then (None,ie) else (Some loc, ie)
       | _ -> (None, exc)
   in
@@ -335,8 +333,7 @@ let rec discard_to_dot () =
  * in encountered. *)
 
 let process_error = function
-  | DuringCommandInterp _
-  | DuringSyntaxChecking _ as e -> e
+  | DuringCommandInterp _ as e -> e
   | e ->
       if is_pervasive_exn e then
 	e
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a00efc5c..9464d763 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 13488 2010-10-03 22:27:05Z herbelin $ *)
+(* $Id: vernac.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -34,8 +34,7 @@ exception HasNotFailed
 let raise_with_file file exc =
   let (cmdloc,re) =
     match exc with
-      | DuringCommandInterp(loc,e)
-      | DuringSyntaxChecking(loc,e) -> (loc,e)
+      | DuringCommandInterp(loc,e) -> (loc,e)
       | e -> (dummy_loc,e)
   in
   let (inner,inex) =
@@ -171,7 +170,7 @@ let rec vernac_com interpfun (loc,com) =
 	  | e ->
 	      (* if [e] is an anomaly, the next function will re-raise it *)
 	      let msg = Cerrors.explain_exn_no_anomaly e in
-	      msgnl (str "The command has indeed failed with message:" ++
+	      if_verbose msgnl (str "The command has indeed failed with message:" ++
 		     fnl () ++ str "=> " ++ hov 0 msg)
 	end
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index b5af665c..0d247189 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 13492 2010-10-04 21:20:01Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 13668 2010-12-02 17:43:59Z herbelin $ i*)
 
 open Util
 open Names
@@ -360,10 +360,7 @@ and located_vernac_expr = loc * vernac_expr
 (* Locating errors raised just after the dot is parsed but before the
    interpretation phase *)
 
-exception DuringSyntaxChecking of exn located
-
-let syntax_checking_error loc s =
-  raise (DuringSyntaxChecking (loc,UserError ("",Pp.str s)))
+let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)
 
 (**********************************************************************)
 (* Managing locality *)