aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml10
-rw-r--r--toplevel/class.ml8
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/locality.ml2
-rw-r--r--toplevel/metasyntax.ml18
-rw-r--r--toplevel/mltop.ml10
-rw-r--r--toplevel/obligations.ml8
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/vernacentries.ml32
-rw-r--r--toplevel/vernacinterp.ml4
13 files changed, 54 insertions, 54 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 180b836ea..d6c2ccad2 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -340,7 +340,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else errorlabstrm "AutoIndDecl.do_replace_lb"
+ else user_err "AutoIndDecl.do_replace_lb"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -398,7 +398,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec find i =
if Id.equal avoid.(n-i) s then avoid.(n-i-x)
else (if i<n then find (i+1)
- else errorlabstrm "AutoIndDecl.do_replace_bl"
+ else user_err "AutoIndDecl.do_replace_bl"
(str "Var " ++ pr_id s ++ str " seems unknown.")
)
in mkVar (find 1)
@@ -506,7 +506,7 @@ let eqI ind l =
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
and e, eff =
try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff
- with Not_found -> errorlabstrm "AutoIndDecl.eqI"
+ with Not_found -> user_err "AutoIndDecl.eqI"
(str "The boolean equality on " ++ pr_mind (fst ind) ++ str " is needed.");
in (if Array.equal eq_constr eA [||] then e else mkApp(e,eA)), eff
@@ -633,7 +633,7 @@ let side_effect_of_mode = function
let make_bl_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- errorlabstrm ""
+ user_err ""
(str "Automatic building of boolean->Leibniz lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
@@ -756,7 +756,7 @@ let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
let make_lb_scheme mode mind =
let mib = Global.lookup_mind mind in
if not (Int.equal (Array.length mib.mind_packets) 1) then
- errorlabstrm ""
+ user_err ""
(str "Automatic building of Leibniz->boolean lemmas not supported");
let ind = (mind,0) in
let nparams = mib.mind_nparams in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 6d53ec9d8..bf17867e8 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -98,7 +98,7 @@ let class_of_global = function
| IndRef sp -> CL_IND sp
| VarRef id -> CL_SECVAR id
| ConstructRef _ as c ->
- errorlabstrm "class_of_global"
+ user_err "class_of_global"
(str "Constructors, such as " ++ Printer.pr_global c ++
str ", cannot be used as a class.")
@@ -177,7 +177,7 @@ let ident_key_of_class = function
(* Identity coercion *)
let error_not_transparent source =
- errorlabstrm "build_id_coercion"
+ user_err "build_id_coercion"
(pr_class source ++ str " must be a transparent constant.")
let build_id_coercion idf_opt source poly =
@@ -208,7 +208,7 @@ let build_id_coercion idf_opt source poly =
(Reductionops.is_conv_leq env sigma
(Typing.unsafe_type_of env sigma val_f) typ_f)
then
- errorlabstrm "" (strbrk
+ user_err "" (strbrk
"Cannot be defined as coercion (maybe a bad number of arguments).")
in
let idf =
@@ -284,7 +284,7 @@ let add_new_coercion_core coef stre poly source target isid =
let try_add_new_coercion_core ref ~local c d e f =
try add_new_coercion_core ref (loc_of_bool local) c d e f
with CoercionError e ->
- errorlabstrm "try_add_new_coercion_core"
+ user_err "try_add_new_coercion_core"
(explain_coercion_error ref e ++ str ".")
let try_add_new_coercion ref ~local poly =
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 26cb7451a..6d62ce24a 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -169,7 +169,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
Name id ->
let sp = Lib.make_path id in
if Nametab.exists_cci sp then
- errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
+ user_err "new_instance" (Nameops.pr_id id ++ Pp.str " already exists.");
id
| Anonymous ->
let i = Nameops.add_suffix (id_of_class k) "_instance_0" in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b9a72fa33..4d333c30d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1312,7 +1312,7 @@ let do_program_fixpoint local poly l =
match n with
| Some n -> mkIdentC (snd n)
| None ->
- errorlabstrm "do_program_fixpoint"
+ user_err "do_program_fixpoint"
(str "Recursive argument required for well-founded fixpoints")
in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
@@ -1326,7 +1326,7 @@ let do_program_fixpoint local poly l =
do_program_recursive local poly fixkind fixl ntns
| _, _ ->
- errorlabstrm "do_program_fixpoint"
+ user_err "do_program_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
let check_safe () =
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index d9cd574a0..b90e62048 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -136,7 +136,7 @@ let get_compat_version = function
| "8.3" -> Flags.V8_3
| "8.2" -> Flags.V8_2
| ("8.1" | "8.0") as s ->
- CErrors.errorlabstrm "get_compat_version"
+ CErrors.user_err "get_compat_version"
(str "Compatibility with version " ++ str s ++ str " not supported.")
- | s -> CErrors.errorlabstrm "get_compat_version"
+ | s -> CErrors.user_err "get_compat_version"
(str "Unknown compatibility version \"" ++ str s ++ str "\".")
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index 6d57a21dc..fee5cffeb 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -87,7 +87,7 @@ let declare_scheme_object s aux f =
try
let _ = Hashtbl.find scheme_object_table key in
(* let aux_msg = if aux="" then "" else " (with key "^aux^")" in*)
- errorlabstrm "IndTables.declare_scheme_object"
+ user_err "IndTables.declare_scheme_object"
(str "Scheme object " ++ str key ++ str " already declared.")
with Not_found ->
Hashtbl.add scheme_object_table key (s,f);
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 154f787ef..7664acbb6 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -18,7 +18,7 @@ let check_locality locality_flag =
match locality_flag with
| Some b ->
let s = if b then "Local" else "Global" in
- CErrors.errorlabstrm "Locality.check_locality"
+ CErrors.user_err "Locality.check_locality"
(str "This command does not support the \"" ++ str s ++ str "\" prefix.")
| None -> ()
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a1edb7139..cef074699 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -238,7 +238,7 @@ let rec find_pattern nt xl = function
| _, Break s :: _ | Break s :: _, _ ->
error ("A break occurs on one side of \"..\" but not on the other side.")
| _, Terminal s :: _ | Terminal s :: _, _ ->
- errorlabstrm "Metasyntax.find_pattern"
+ user_err "Metasyntax.find_pattern"
(str "The token \"" ++ str s ++ str "\" occurs on one side of \"..\" but not on the other side.")
| _, [] ->
error msg_expected_form_of_recursive_notation
@@ -300,7 +300,7 @@ let rec get_notation_vars = function
let vars = get_notation_vars sl in
if Id.equal id ldots_var then vars else
if Id.List.mem id vars then
- errorlabstrm "Metasyntax.get_notation_vars"
+ user_err "Metasyntax.get_notation_vars"
(str "Variable " ++ pr_id id ++ str " occurs more than once.")
else
id::vars
@@ -314,7 +314,7 @@ let analyze_notation_tokens l =
recvars, List.subtract Id.equal vars (List.map snd recvars), l
let error_not_same_scope x y =
- errorlabstrm "Metasyntax.error_not_name_scope"
+ user_err "Metasyntax.error_not_name_scope"
(str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.")
(**********************************************************************)
@@ -390,7 +390,7 @@ let check_open_binder isopen sl m =
| _ -> assert false
in
if isopen && not (List.is_empty sl) then
- errorlabstrm "" (str "as " ++ pr_id m ++
+ user_err "" (str "as " ++ pr_id m ++
str " is a non-closed binder, no such \"" ++
prlist_with_sep spc pr_token sl
++ strbrk "\" is allowed to occur.")
@@ -661,7 +661,7 @@ let pr_level ntn (from,args) =
prlist_with_sep pr_comma (pr_arg_level from) args
let error_incompatible_level ntn oldprec prec =
- errorlabstrm ""
+ user_err ""
(str "Notation " ++ str ntn ++ str " is already defined" ++ spc() ++
pr_level ntn oldprec ++
spc() ++ str "while it is now required to be" ++ spc() ++
@@ -731,7 +731,7 @@ let interp_modifiers modl =
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- errorlabstrm "Metasyntax.interp_modifiers"
+ user_err "Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
interp assoc level ((id,typ)::etyps) format extra l
| SetItemLevel ([],n) :: l ->
@@ -739,7 +739,7 @@ let interp_modifiers modl =
| SetItemLevel (s::idl,n) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
- errorlabstrm "Metasyntax.interp_modifiers"
+ user_err "Metasyntax.interp_modifiers"
(str s ++ str " is already assigned to an entry or constr level.");
let typ = ETConstr (n,()) in
interp assoc level ((id,typ)::etyps) format extra (SetItemLevel (idl,n)::l)
@@ -770,7 +770,7 @@ let check_infix_modifiers modifiers =
let check_useless_entry_types recvars mainvars etyps =
let vars = let (l1,l2) = List.split recvars in l1@l2@mainvars in
match List.filter (fun (x,etyp) -> not (List.mem x vars)) etyps with
- | (x,_)::_ -> errorlabstrm "Metasyntax.check_useless_entry_types"
+ | (x,_)::_ -> user_err "Metasyntax.check_useless_entry_types"
(pr_id x ++ str " is unbound in the notation.")
| _ -> ()
@@ -813,7 +813,7 @@ let join_auxiliary_recursive_types recvars etyps =
| None, Some ytyp -> (x,ytyp)::typs
| Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *)
| Some xtyp, Some ytyp ->
- errorlabstrm ""
+ user_err ""
(strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++
strbrk ", both ends have incompatible types."))
recvars etyps
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fbd1e6033..c74c3522d 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -124,13 +124,13 @@ let ml_load s =
| (UserError _ | Failure _ | Not_found as u) -> Exninfo.iraise (u, snd e)
| exc ->
let msg = report_on_load_obj_error exc in
- errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
+ user_err "Mltop.load_object" (str"Cannot link ml-object " ++
str s ++ str" to Coq code (" ++ msg ++ str ")."))
| WithoutTop ->
try
Dynlink.loadfile s; s
with Dynlink.Error a ->
- errorlabstrm "Mltop.load_object"
+ user_err "Mltop.load_object"
(strbrk "while loading " ++ str s ++
strbrk ": " ++ str (Dynlink.error_message a))
@@ -151,7 +151,7 @@ let dir_ml_use s =
if Dynlink.is_native then " Loading ML code works only in bytecode."
else ""
in
- errorlabstrm "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
+ user_err "Mltop.dir_ml_use" (str "Could not load ML code." ++ str moreinfo)
(* Adds a path to the ML paths *)
let add_ml_dir s =
@@ -221,7 +221,7 @@ let get_ml_object_suffix name =
let file_of_name name =
let suffix = get_ml_object_suffix name in
let fail s =
- errorlabstrm "Mltop.load_object"
+ user_err "Mltop.load_object"
(str"File not found on loadpath : " ++ str s ++ str"\n" ++
str"Loadpath: " ++ str(String.concat ":" !coq_mlpath_copy)) in
if not (Filename.is_relative name) then
@@ -355,7 +355,7 @@ let trigger_ml_object verb cache reinit ?path name =
add_loaded_module name (known_module_path name);
if cache then perform_cache_obj name
end else if not has_dynlink then
- errorlabstrm "Mltop.trigger_ml_object"
+ user_err "Mltop.trigger_ml_object"
(str "Dynamic link not supported (module " ++ str name ++ str ")")
else begin
let file = file_of_name (Option.default name path) in
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 38d4a62b4..b9fd2894d 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -258,7 +258,7 @@ let safe_init_constant md name () =
Coqlib.gen_constant "Obligations" md name
let hide_obligation = safe_init_constant tactics_module "obligation"
-let pperror cmd = CErrors.errorlabstrm "Program" cmd
+let pperror cmd = CErrors.user_err "Program" cmd
let error s = pperror (str s)
let reduce c =
@@ -398,7 +398,7 @@ let rec prod_app t n =
| Prod (_,_,b) -> subst1 n b
| LetIn (_, b, t, b') -> prod_app (subst1 b b') n
| _ ->
- errorlabstrm "prod_app"
+ user_err "prod_app"
(str"Needed a product, but didn't find one" ++ fnl ())
@@ -444,7 +444,7 @@ let from_prg : program_info ProgMap.t ref =
let close sec =
if not (ProgMap.is_empty !from_prg) then
let keys = map_keys !from_prg in
- errorlabstrm "Program"
+ user_err "Program"
(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++
(str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
@@ -718,7 +718,7 @@ let get_prog name =
let progs = Id.Set.elements (ProgMap.domain prg_infos) in
let prog = List.hd progs in
let progs = prlist_with_sep pr_comma Nameops.pr_id progs in
- errorlabstrm ""
+ user_err ""
(str "More than one program with unsolved obligations: " ++ progs
++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Nameops.pr_id prog ++ str "\""))
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 6a64b0d66..22dc8c957 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -208,7 +208,7 @@ let warning_or_error coe indsp err =
| _ ->
(pr_id fi ++ strbrk " cannot be defined because it is not typable.")
in
- if coe then errorlabstrm "structure" st;
+ if coe then user_err "structure" st;
Flags.if_verbose Feedback.msg_info (hov 0 st)
type field_status =
@@ -235,7 +235,7 @@ let subst_projection fid l c =
| Projection t -> lift depth t
| NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
| NoProjection Anonymous ->
- errorlabstrm "" (str "Field " ++ pr_id fid ++
+ user_err "" (str "Field " ++ pr_id fid ++
str " depends on the " ++ pr_nth (k-depth-1) ++ str
" field which has no name.")
else
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 3f784fd8a..9e3494145 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -483,7 +483,7 @@ let vernac_start_proof locality p kind l lettop =
| None -> ()) l;
if not(refining ()) then
if lettop then
- errorlabstrm "Vernacentries.StartProof"
+ user_err "Vernacentries.StartProof"
(str "Let declarations can only be used in proof editing mode.");
start_proof_and_print (local, p, Proof kind) l no_hook
@@ -855,7 +855,7 @@ let vernac_set_used_variables e =
let vars = Environ.named_context env in
List.iter (fun id ->
if not (List.exists (Id.equal id % get_id) vars) then
- errorlabstrm "vernac_set_used_variables"
+ user_err "vernac_set_used_variables"
(str "Unknown variable: " ++ pr_id id))
l;
let _, to_clear = set_used_variables l in
@@ -974,9 +974,9 @@ let vernac_declare_arguments locality r l nargs flags =
| [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls
| [], _::_, (Some _)::ls when extra_scope_flag ->
error "Extra notation scopes can be set on anonymous arguments only"
- | [], x::_, _ -> errorlabstrm "vernac_declare_arguments"
+ | [], x::_, _ -> user_err "vernac_declare_arguments"
(str "Extra argument " ++ pr_name x ++ str ".")
- | l, [], _ -> errorlabstrm "vernac_declare_arguments"
+ | l, [], _ -> user_err "vernac_declare_arguments"
(str "The following arguments are not declared: " ++
prlist_with_sep pr_comma pr_name l ++ str ".")
| _::li, _::ld, _::ls -> check li ld ls
@@ -1019,7 +1019,7 @@ let vernac_declare_arguments locality r l nargs flags =
let sr', impl = List.fold_map (fun b -> function
| (Anonymous, _,_, true, max), Name id -> assert false
| (Name x, _,_, true, _), Anonymous ->
- errorlabstrm "vernac_declare_arguments"
+ user_err "vernac_declare_arguments"
(str "Argument " ++ pr_id x ++ str " cannot be declared implicit.")
| (Name iid, _,_, true, max), Name id ->
set_renamed iid id;
@@ -1033,7 +1033,7 @@ let vernac_declare_arguments locality r l nargs flags =
some_renaming_specified l in
if some_renaming_specified then
if not (List.mem `Rename flags) then
- errorlabstrm "vernac_declare_arguments"
+ user_err "vernac_declare_arguments"
(str "To rename arguments the \"rename\" flag must be specified." ++
match !renamed_arg with
| None -> mt ()
@@ -1077,7 +1077,7 @@ let vernac_declare_arguments locality r l nargs flags =
| ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
(make_section_locality locality) c (rargs, nargs, flags)
- | _ -> errorlabstrm "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+ | _ -> user_err "" (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
end;
if not (some_renaming_specified ||
some_implicits_specified ||
@@ -1498,7 +1498,7 @@ 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 _ -> errorlabstrm "print_about_hyp_globs"
+ Failure _ -> user_err "print_about_hyp_globs"
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
@@ -1597,7 +1597,7 @@ let interp_search_about_item env =
(fun _ -> true) s sc in
GlobSearchSubPattern (Pattern.PRef ref)
with UserError _ ->
- errorlabstrm "interp_search_about_item"
+ user_err "interp_search_about_item"
(str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component")
let vernac_search s gopt r =
@@ -1877,12 +1877,12 @@ let interp ?proof ~loc locality poly c =
| VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n")
(* The STM should handle that, but LOAD bypasses the STM... *)
- | VernacAbort id -> CErrors.errorlabstrm "" (str "Abort cannot be used through the Load command")
- | VernacAbortAll -> CErrors.errorlabstrm "" (str "AbortAll cannot be used through the Load command")
- | VernacRestart -> CErrors.errorlabstrm "" (str "Restart cannot be used through the Load command")
- | VernacUndo _ -> CErrors.errorlabstrm "" (str "Undo cannot be used through the Load command")
- | VernacUndoTo _ -> CErrors.errorlabstrm "" (str "UndoTo cannot be used through the Load command")
- | VernacBacktrack _ -> CErrors.errorlabstrm "" (str "Backtrack cannot be used through the Load command")
+ | VernacAbort id -> CErrors.user_err "" (str "Abort cannot be used through the Load command")
+ | VernacAbortAll -> CErrors.user_err "" (str "AbortAll cannot be used through the Load command")
+ | VernacRestart -> CErrors.user_err "" (str "Restart cannot be used through the Load command")
+ | VernacUndo _ -> CErrors.user_err "" (str "Undo cannot be used through the Load command")
+ | VernacUndoTo _ -> CErrors.user_err "" (str "UndoTo cannot be used through the Load command")
+ | VernacBacktrack _ -> CErrors.user_err "" (str "Backtrack cannot be used through the Load command")
(* Proof management *)
| VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false
@@ -2014,7 +2014,7 @@ let with_fail b f =
let (e, _) = CErrors.push e in
match e with
| HasNotFailed ->
- errorlabstrm "Fail" (str "The command has not failed!")
+ user_err "Fail" (str "The command has not failed!")
| HasFailed msg ->
if is_verbose () || !test_mode || !ide_slave then Feedback.msg_info
(str "The command has indeed failed with message:" ++ fnl () ++ msg)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index d81e3d6b5..147727e7c 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -22,7 +22,7 @@ let vinterp_add depr s f =
try
Hashtbl.add vernac_tab s (depr, f)
with Failure _ ->
- errorlabstrm "vinterp_add"
+ user_err "vinterp_add"
(str"Cannot add the vernac command " ++ str (fst s) ++ str" twice.")
let overwriting_vinterp_add s f =
@@ -37,7 +37,7 @@ let vinterp_map s =
try
Hashtbl.find vernac_tab s
with Failure _ | Not_found ->
- errorlabstrm "Vernac Interpreter"
+ user_err "Vernac Interpreter"
(str"Cannot find vernac command " ++ str (fst s) ++ str".")
let vinterp_init () = Hashtbl.clear vernac_tab
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:41:51 +0000