aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/notation.mli6
-rw-r--r--plugins/syntax/numeral.ml32
-rw-r--r--proofs/logic.ml1
-rw-r--r--vernac/explainErr.ml2
-rw-r--r--vernac/himsg.ml10
-rw-r--r--vernac/himsg.mli2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:34:27 +0000