Remove VernacError

1 files changed, 19 insertions, 13 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 92b1a5956..52136a70e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1533,7 +1533,14 @@ let get_current_context_of_args = function
   | Some n -> get_goal_context n
   | None -> get_current_context ()
 
-let vernac_check_may_eval redexp glopt rc =
+let query_command_selector ~loc = function
+  | None -> None
+  | Some (SelectNth n) -> Some n
+  | _ -> user_err ~loc ~hdr:"query_command_selector"
+      (str "Query commands only support the single numbered goal selector.")
+
+let vernac_check_may_eval ~loc redexp glopt rc =
+  let glopt = query_command_selector ~loc glopt in
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
   let c = EConstr.Unsafe.to_constr c in
@@ -1595,9 +1602,10 @@ exception NoHyp
 (* Printing "About" information of a hypothesis of the current goal.
    We only print the type and a small statement to this comes from the
    goal. Precondition: there must be at least one current goal. *)
-let print_about_hyp_globs ref_or_by_not glnumopt =
+let print_about_hyp_globs ~loc ref_or_by_not glopt =
   let open Context.Named.Declaration in
   try
+    let glnumopt = query_command_selector ~loc glopt in
     let gl,id =
       match glnumopt,ref_or_by_not with
       | None,AN (Ident (_loc,id)) -> (* goal number not given, catch any failure *)
@@ -1605,8 +1613,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
       | Some n,AN (Ident (_loc,id)) ->  (* goal number given, catch if wong *)
 	 (try get_nth_goal n,id
 	  with
-	    Failure _ -> user_err ~hdr:"print_about_hyp_globs"
-                           (str "No such goal: " ++ int n ++ str "."))
+	    Failure _ -> user_err ~loc ~hdr:"print_about_hyp_globs"
+                          (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
     let decl = Context.Named.lookup id hyps in
@@ -1619,7 +1627,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
     | NoHyp | Not_found -> print_about ref_or_by_not
 
 	       
-let vernac_print = let open Feedback in function
+let vernac_print ~loc = let open Feedback in function
   | PrintTables -> msg_notice (print_tables ())
   | PrintFullContext-> msg_notice (print_full_context_typ ())
   | PrintSectionContext qid -> msg_notice (print_sec_context_typ qid)
@@ -1664,7 +1672,7 @@ let vernac_print = let open Feedback in function
   | PrintVisibility s ->
       msg_notice (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintAbout (ref_or_by_not,glnumopt) ->
-     msg_notice (print_about_hyp_globs ref_or_by_not glnumopt)
+     msg_notice (print_about_hyp_globs ~loc ref_or_by_not glnumopt)
   | PrintImplicit qid ->
     dump_global qid; msg_notice (print_impargs qid)
   | PrintAssumptions (o,t,r) ->
@@ -1729,7 +1737,8 @@ let _ =
       optread  = (fun () -> !search_output_name_only);
       optwrite = (:=) search_output_name_only }
 
-let vernac_search s gopt r =
+let vernac_search ~loc s gopt r =
+  let gopt = query_command_selector ~loc gopt in
   let r = interp_search_restriction r in
   let env,gopt =
     match gopt with | None ->
@@ -1935,9 +1944,6 @@ let interp ?proof ~loc locality poly c =
   | VernacBack _       -> anomaly (str "VernacBack not handled by Stm")
   | VernacBackTo _     -> anomaly (str "VernacBackTo not handled by Stm")
 
-  (* Horrible Hack that should die. *)
-  | VernacError e -> raise e
-
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
 
@@ -2039,11 +2045,11 @@ let interp ?proof ~loc locality poly c =
   | VernacAddOption (key,v) -> vernac_add_option key v
   | VernacMemOption (key,v) -> vernac_mem_option key v
   | VernacPrintOption key -> vernac_print_option key
-  | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval r g c
+  | VernacCheckMayEval (r,g,c) -> vernac_check_may_eval ~loc r g c
   | VernacDeclareReduction (s,r) -> vernac_declare_reduction locality s r
   | VernacGlobalCheck c -> vernac_global_check c
-  | VernacPrint p -> vernac_print p
-  | VernacSearch (s,g,r) -> vernac_search s g r
+  | VernacPrint p -> vernac_print ~loc p
+  | VernacSearch (s,g,r) -> vernac_search ~loc s g r
   | VernacLocate l -> vernac_locate l
   | VernacRegister (id, r) -> vernac_register id r
   | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")