diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/lemmas.ml | 14 | ||||
| -rw-r--r-- | stm/stm.ml | 14 |
2 files changed, 15 insertions, 13 deletions
diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 022c89ad9a..55f33be399 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -33,6 +33,9 @@ open Constrintern open Impargs open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration + type 'a declaration_hook = Decl_kinds.locality -> Globnames.global_reference -> 'a let mk_hook hook = hook let call_hook fix_exn hook l c = @@ -45,8 +48,7 @@ let call_hook fix_exn hook l c = let retrieve_first_recthm = function | VarRef id -> - let open Context.Named.Declaration in - (get_value (Global.lookup_named id),variable_opacity id) + (NamedDecl.get_value (Global.lookup_named id),variable_opacity id) | ConstRef cst -> let cb = Global.lookup_constant cst in (Global.body_of_constant_body cb, is_opaque cb) @@ -110,7 +112,7 @@ let find_mutually_recursive_statements thms = (Global.env()) hyps in let ind_hyps = List.flatten (List.map_i (fun i decl -> - let t = get_type decl in + let t = RelDecl.get_type decl in match kind_of_term t with | Ind ((kn,_ as ind),u) when let mind = Global.lookup_mind kn in @@ -222,7 +224,7 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err_loc (loc,"",pr_id id ++ str " already exists."); + user_err ~loc (pr_id id ++ str " already exists."); id, pl | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None @@ -335,7 +337,7 @@ let get_proof proof do_guard hook opacity = let check_exist = List.iter (fun (loc,id) -> if not (Nametab.exists_cci (Lib.make_path id)) then - user_err_loc (loc,"",pr_id id ++ str " does not exist.") + user_err ~loc (pr_id id ++ str " does not exist.") ) let universe_proof_terminator compute_guard hook = @@ -462,7 +464,7 @@ let start_proof_com ?inference_hook kind thms hook = let flags = all_and_fail_flags in let flags = { flags with use_hook = inference_hook } in evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); - let ids = List.map get_name ctx in + let ids = List.map RelDecl.get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (List.length ids) imps'), diff --git a/stm/stm.ml b/stm/stm.ml index bb4f5f72f3..3fd844f351 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1040,7 +1040,7 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - CErrors.errorlabstrm "undo_vernac_classifier" + CErrors.user_err ~hdr:"undo_vernac_classifier" (str "Cannot undo") end (* }}} *) @@ -1108,7 +1108,7 @@ let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then - CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name); + CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name); proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters let mk_doc_node id = function @@ -1143,7 +1143,7 @@ let detect_proof_block id name = VCS.create_proof_block decl name end with Not_found -> - CErrors.errorlabstrm "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) @@ -1708,7 +1708,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^ + CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1721,7 +1721,7 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.errorlabstrm "STM" (str"The solution is not ground") + else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) @@ -2058,7 +2058,7 @@ let known_state ?(redefine_qed=false) ~cache id = | _ -> assert false end with Not_found -> - CErrors.errorlabstrm "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) in @@ -2410,7 +2410,7 @@ let handle_failure (e, info) vcs tty = let snapshot_vio ldir long_f_dot_vo = finish (); if List.length (VCS.branches ()) > 1 then - CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); + CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo (Global.opaque_tables ()) |