diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | interp/coqlib.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 4 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 | ||||
| -rw-r--r-- | interp/syntax_def.ml | 2 |
5 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f4907e92a..82039abd3 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -366,7 +366,7 @@ let check_hidden_implicit_parameters id impls = | (Inductive indparams,_,_,_) -> Id.List.mem id indparams | _ -> false) impls then - errorlabstrm "" (strbrk "A parameter of an inductive type " ++ + user_err "" (strbrk "A parameter of an inductive type " ++ pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") let push_name_env ?(global_level=false) ntnvars implargs env = diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 588637b76..19f76b972 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -86,7 +86,7 @@ let check_required_library d = (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m) *) (* or failing ...*) - errorlabstrm "Coqlib.check_required_library" + user_err "Coqlib.check_required_library" (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") (************************************************************************) diff --git a/interp/notation.ml b/interp/notation.ml index 0c15e91b8..d50045546 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -95,7 +95,7 @@ let declare_scope scope = scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = - errorlabstrm "Notation" + user_err "Notation" (str "Scope " ++ str sc ++ str " is not declared.") let find_scope scope = @@ -208,7 +208,7 @@ let remove_delimiters scope = let sc = find_scope scope in let newsc = { sc with delimiters = None } in match sc.delimiters with - | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".") + | None -> CErrors.user_err "" (str "No bound key for scope " ++ str scope ++ str ".") | Some key -> scope_map := String.Map.add scope newsc !scope_map; try diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7ab6ebb26..d565f01ba 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -377,7 +377,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = let vars = Id.Map.filter filter nenv.ninterp_var_type in let check_recvar x = if Id.List.mem x found then - errorlabstrm "" (pr_id x ++ + user_err "" (pr_id x ++ strbrk " should only be used in the recursive part of a pattern.") in let check (x, y) = check_recvar x; check_recvar y in let () = List.iter check foundrec in @@ -396,7 +396,7 @@ let check_variables nenv (found,foundrec,foundrecbinding) = in let check_pair s x y where = if not (List.mem_f (pair_equal Id.equal Id.equal) (x,y) where) then - errorlabstrm "" (strbrk "in the right-hand side, " ++ pr_id x ++ + user_err "" (strbrk "in the right-hand side, " ++ pr_id x ++ str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index f96d8acc1..1e0964dd2 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -30,7 +30,7 @@ let add_syntax_constant kn c onlyparse = let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = if Nametab.exists_cci sp then - errorlabstrm "cache_syntax_constant" + user_err "cache_syntax_constant" (pr_id (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn |