summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/cerrors.ml13
-rw-r--r--toplevel/command.ml6
-rw-r--r--toplevel/metasyntax.ml28
-rw-r--r--toplevel/toplevel.ml9
-rw-r--r--toplevel/vernac.ml7
-rw-r--r--toplevel/vernacexpr.ml7
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 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-28 05:57:24 +0000