Fix Numeral Notations (2/4 - exceptions, usr_err)

Switch to using exceptions rather than user errors.  This will be
required because the machinery for printing constrs is not available in
notation.ml, so we move the error message printing to himsg.ml instead.

This is commit 2/4 in the fix for #8401.

7 files changed, 39 insertions, 20 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 8cb423051a..25772d8fe4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -389,6 +389,12 @@ let prim_token_uninterpreters =
 
 (*******************************************************)
 (* Numeral notation interpretation                     *)
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
 type numnot_option =
   | Nop
   | Warning of raw_natural_number
diff --git a/interp/notation.mli b/interp/notation.mli
index 7f20a2ef1f..33e275d925 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -104,6 +104,12 @@ val register_string_interpretation :
 
 (** * Numeral notation *)
 
+type numeral_notation_error =
+  | UnexpectedTerm of Constr.t
+  | UnexpectedNonOptionTerm of Constr.t
+
+exception NumeralNotationError of Environ.env * Evd.evar_map * numeral_notation_error
+
 type numnot_option =
   | Nop
   | Warning of raw_natural_number
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 7acf18da2f..bc25e4730d 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -63,14 +63,14 @@ let warn_abstract_large_num =
     (fun (ty,f) ->
       strbrk "To avoid stack overflow, large numbers in " ++
       pr_qualid ty ++ strbrk " are interpreted as applications of " ++
-      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
+      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ".")
 
 let warn_abstract_large_num_no_op =
   CWarnings.create ~name:"abstract-large-number-no-op" ~category:"numbers"
     (fun f ->
       strbrk "The 'abstract after' directive has no effect when " ++
       strbrk "the parsing function (" ++
-      Printer.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
+      Nametab.pr_global_env (Termops.vars_of_env (Global.env ())) f ++ strbrk ") targets an " ++
       strbrk "option type.")
 
 (** Comparing two raw numbers (base 10, big-endian, non-negative).
@@ -224,35 +224,27 @@ let rec constr_of_glob env sigma g = match DAst.get g with
   | _ ->
       raise NotANumber
 
-let rec glob_of_constr ?loc c = match Constr.kind c with
+let rec glob_of_constr ?loc env sigma c = match Constr.kind c with
   | App (c, ca) ->
-      let c = glob_of_constr ?loc c in
-      let cel = List.map (glob_of_constr ?loc) (Array.to_list ca) in
+      let c = glob_of_constr ?loc env sigma c in
+      let cel = List.map (glob_of_constr ?loc env sigma) (Array.to_list ca) in
       DAst.make ?loc (Glob_term.GApp (c, cel))
   | Construct (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstructRef c, None))
   | Const (c, _) -> DAst.make ?loc (Glob_term.GRef (ConstRef c, None))
   | Ind (ind, _) -> DAst.make ?loc (Glob_term.GRef (IndRef ind, None))
   | Var id -> DAst.make ?loc (Glob_term.GRef (VarRef id, None))
-  | _ -> let (sigma, env) = Pfedit.get_current_context () in
-         CErrors.user_err ?loc
-           (strbrk "Unexpected term " ++
-              Printer.pr_constr_env env sigma c ++
-              strbrk " while parsing a numeral notation.")
+  | _ -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedTerm c))
 
 let no_such_number ?loc ty =
   CErrors.user_err ?loc
    (str "Cannot interpret this number as a value of type " ++
     pr_qualid ty)
 
-let interp_option ty ?loc c =
+let interp_option ty ?loc env sigma c =
   match Constr.kind c with
-  | App (_Some, [| _; c |]) -> glob_of_constr ?loc c
+  | App (_Some, [| _; c |]) -> glob_of_constr ?loc env sigma c
   | App (_None, [| _ |]) -> no_such_number ?loc ty
-  | x -> let (sigma, env) = Pfedit.get_current_context () in
-         CErrors.user_err ?loc
-          (strbrk "Unexpected non-option term " ++
-             Printer.pr_constr_env env sigma c ++
-             strbrk " while parsing a numeral notation.")
+  | x -> Loc.raise ?loc (NumeralNotationError(env,sigma,UnexpectedNonOptionTerm c))
 
 let uninterp_option c =
   match Constr.kind c with
@@ -285,12 +277,12 @@ let interp o ?loc n =
   match o.warning, snd o.to_kind with
   | Abstract threshold, Direct when rawnum_compare (fst n) threshold >= 0 ->
      warn_abstract_large_num (o.num_ty,o.to_ty);
-     glob_of_constr ?loc (mkApp (to_ty,[|c|]))
+     glob_of_constr ?loc env sigma (mkApp (to_ty,[|c|]))
   | _ ->
      let res = eval_constr_app env sigma to_ty c in
      match snd o.to_kind with
-     | Direct -> glob_of_constr ?loc res
-     | Option -> interp_option o.num_ty ?loc res
+     | Direct -> glob_of_constr ?loc env sigma res
+     | Option -> interp_option o.num_ty ?loc env sigma res
 
 let uninterp o (Glob_term.AnyGlobConstr n) =
   let env = Global.env () in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e8ca719932..613581ade7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,7 @@ let is_unification_error = function
 
 let catchable_exception = function
   | CErrors.UserError _ | TypeError _
+  | Notation.NumeralNotationError _
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _
   (* reduction errors *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index 504e7095b0..7cf4e64805 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -64,6 +64,8 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_type_error ctx Evd.empty te)
   | PretypeError(ctx,sigma,te) ->
       wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
+  | Notation.NumeralNotationError(ctx,sigma,te) ->
+      wrap_vernac_error exn (Himsg.explain_numeral_notation_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
       wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
   | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a4650cfd92..e7b2a0e8a6 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1315,3 +1315,13 @@ let explain_reduction_tactic_error = function
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' (Evd.from_env env') e
+
+let explain_numeral_notation_error env sigma = function
+  | Notation.UnexpectedTerm c ->
+    (strbrk "Unexpected term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")
+  | Notation.UnexpectedNonOptionTerm c ->
+    (strbrk "Unexpected non-option term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 91caddcf13..02b3c45501 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -46,3 +46,5 @@ val explain_module_internalization_error :
 
 val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error
 val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error
+
+val explain_numeral_notation_error : env -> Evd.evar_map -> Notation.numeral_notation_error -> Pp.t