diff options
| -rw-r--r-- | interp/constrintern.ml | 4 | ||||
| -rw-r--r-- | interp/topconstr.ml | 2 | ||||
| -rw-r--r-- | interp/topconstr.mli | 2 | ||||
| -rw-r--r-- | parsing/egramcoq.ml | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index fb11359e3c..0e56020783 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1208,7 +1208,7 @@ let drop_notations_pattern looked_for = if top then looked_for g else match g with ConstructRef _ -> () | _ -> raise Not_found with Not_found -> - error_invalid_pattern_notation ~loc + error_invalid_pattern_notation ~loc () in let test_kind top = if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found @@ -1349,7 +1349,7 @@ let drop_notations_pattern looked_for = | NHole _ -> let () = assert (List.is_empty args) in RCPatAtom (loc, None) - | t -> error_invalid_pattern_notation ~loc + | t -> error_invalid_pattern_notation ~loc () in in_pat true let rec intern_pat genv aliases pat = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 0f894019b0..eb564f3b32 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -32,7 +32,7 @@ let _ = Goptions.declare_bool_option { (**********************************************************************) (* Miscellaneous *) -let error_invalid_pattern_notation ?loc = +let error_invalid_pattern_notation ?loc () = user_err ?loc (str "Invalid notation for pattern.") (**********************************************************************) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index ac98331c6b..95d702f8d5 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -46,4 +46,4 @@ val patntn_loc : (** For cases pattern parsing errors *) -val error_invalid_pattern_notation : ?loc:Loc.t -> 'a +val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 0dbe082311..9560bf2a3b 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -434,7 +434,7 @@ let make_act : type r. r target -> _ -> r gen_eval = function CNotation (loc, notation , env) | ForPattern -> fun notation loc env -> let invalid = List.exists (fun (_, b) -> not b) env.binders in - let () = if invalid then Topconstr.error_invalid_pattern_notation loc in + let () = if invalid then Topconstr.error_invalid_pattern_notation ~loc () in let env = (env.constrs, env.constrlists) in CPatNotation (loc, notation, env, []) |