aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/declare.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/declare.ml')
-rw-r--r--interp/declare.ml21
1 files changed, 10 insertions, 11 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 0cc4d0fca..1a589897b 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -14,7 +14,6 @@ open Util
open Names
open Libnames
open Globnames
-open Nameops
open Constr
open Declarations
open Entries
@@ -46,7 +45,7 @@ let cache_variable ((sp,_),o) =
| Inr (id,(p,d,mk)) ->
(* Constr raisonne sur les noms courts *)
if variable_exists id then
- alreadydeclared (pr_id id ++ str " already exists");
+ alreadydeclared (Id.print id ++ str " already exists");
let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
| SectionLocalAssum ((ty,ctx),poly,impl) ->
@@ -107,7 +106,7 @@ type constant_declaration = Safe_typing.private_constants constant_entry * logic
(* section (if Remark or Fact) is needed to access a construction *)
let load_constant i ((sp,kn), obj) =
if Nametab.exists_cci sp then
- alreadydeclared (pr_id (basename sp) ++ str " already exists");
+ alreadydeclared (Id.print (basename sp) ++ str " already exists");
let con = Global.constant_of_delta_kn kn in
Nametab.push (Nametab.Until i) sp (ConstRef con);
add_constant_kind con obj.cst_kind
@@ -132,7 +131,7 @@ let exists_name id =
let check_exists sp =
let id = basename sp in
- if exists_name id then alreadydeclared (pr_id id ++ str " already exists")
+ if exists_name id then alreadydeclared (Id.print id ++ str " already exists")
let cache_constant ((sp,kn), obj) =
let id = basename sp in
@@ -407,11 +406,11 @@ let pr_rank i = pr_nth (i+1)
let fixpoint_message indexes l =
Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "no recursive definition.")
- | [id] -> pr_id id ++ str " is recursively defined" ++
+ | [id] -> Id.print id ++ str " is recursively defined" ++
(match indexes with
| Some [|i|] -> str " (decreasing on "++pr_rank i++str " argument)"
| _ -> mt ())
- | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+ | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
spc () ++ str "are recursively defined" ++
match indexes with
| Some a -> spc () ++ str "(decreasing respectively on " ++
@@ -422,21 +421,21 @@ let fixpoint_message indexes l =
let cofixpoint_message l =
Flags.if_verbose Feedback.msg_info (match l with
| [] -> anomaly (Pp.str "No corecursive definition.")
- | [id] -> pr_id id ++ str " is corecursively defined"
- | l -> hov 0 (prlist_with_sep pr_comma pr_id l ++
+ | [id] -> Id.print id ++ str " is corecursively defined"
+ | l -> hov 0 (prlist_with_sep pr_comma Id.print l ++
spc () ++ str "are corecursively defined"))
let recursive_message isfix i l =
(if isfix then fixpoint_message i else cofixpoint_message) l
let definition_message id =
- Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
let assumption_message id =
(* Changing "assumed" to "declared", "assuming" referring more to
the type of the object than to the name of the object (see
discussion on coqdev: "Chapter 4 of the Reference Manual", 8/10/2015) *)
- Flags.if_verbose Feedback.msg_info (pr_id id ++ str " is declared")
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is declared")
(** Global universe names, in a different summary *)
@@ -527,7 +526,7 @@ let do_constraint poly l =
let names, _ = Global.global_universe_names () in
try loc, Id.Map.find id names
with Not_found ->
- user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id)
+ user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ Id.print id)
in
let in_section = Lib.sections_are_opened () in
let () =