diff options
50 files changed, 261 insertions, 259 deletions
diff --git a/API/API.mli b/API/API.mli index cb945179f..704f1a356 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1863,6 +1863,9 @@ end module Nameops : sig + + open Names + val atompart_of_id : Names.Id.t -> string val pr_id : Names.Id.t -> Pp.t @@ -1871,19 +1874,28 @@ sig val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] - val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a - val name_app : (Names.Id.t -> Names.Id.t) -> Names.Name.t -> Names.Name.t - val add_suffix : Names.Id.t -> string -> Names.Id.t - val increment_subscript : Names.Id.t -> Names.Id.t - val make_ident : string -> int option -> Names.Id.t - val out_name : Names.Name.t -> Names.Id.t - val pr_lab : Names.Label.t -> Pp.t - module Name : - sig - include module type of struct include Names.Name end + module Name : sig + include module type of struct include Name end + + val map : (Id.t -> Id.t) -> Name.t -> t val get_id : t -> Names.Id.t val fold_right : (Names.Id.t -> 'a -> 'a) -> t -> 'a -> 'a + end + + val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a + [@@ocaml.deprecated "alias of API.Names"] + + val name_app : (Id.t -> Id.t) -> Name.t -> Name.t + [@@ocaml.deprecated "alias of API.Names"] + + val add_suffix : Id.t -> string -> Id.t + val increment_subscript : Id.t -> Id.t + val make_ident : string -> int option -> Id.t + val out_name : Name.t -> Id.t + [@@ocaml.deprecated "alias of API.Names"] + val pr_lab : Label.t -> Pp.t + [@@ocaml.deprecated "alias of API.Names"] end module Libnames : diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e48abce1c..b4c8ae33c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -14,7 +14,6 @@ open Pp open Names open Libnames open Globnames -open Nameops open Univ open Environ open Printer @@ -38,7 +37,7 @@ let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) (* name printers *) let ppid id = pp (Id.print id) -let pplab l = pp (pr_lab l) +let pplab l = pp (Label.print l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) let ppmp mp = pp(str (ModPath.debug_to_string mp)) diff --git a/engine/evd.ml b/engine/evd.ml index a1cb0ec68..8d465384b 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -380,7 +380,7 @@ let add_name_newly_undefined id evk evi (evtoid, idtoev as names) = | None -> names | Some id -> if Id.Map.mem id idtoev then - user_err (str "Already an existential evar of name " ++ pr_id id); + user_err (str "Already an existential evar of name " ++ Id.print id); (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = diff --git a/engine/termops.ml b/engine/termops.ml index 78dbdb11a..46fac50f2 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -50,13 +50,13 @@ let pr_puniverses p u = let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" - | Var id -> pr_id id + | Var id -> Id.print id | Sort s -> print_sort s | Cast (c,_, t) -> hov 1 (str"(" ++ pr_constr c ++ cut() ++ str":" ++ pr_constr t ++ str")") | Prod (Name(id),t,c) -> hov 1 - (str"forall " ++ pr_id id ++ str":" ++ pr_constr t ++ str"," ++ + (str"forall " ++ Id.print id ++ str":" ++ pr_constr t ++ str"," ++ spc() ++ pr_constr c) | Prod (Anonymous,t,c) -> hov 0 (str"(" ++ pr_constr t ++ str " ->" ++ spc() ++ @@ -130,9 +130,9 @@ let pr_existential_key sigma evk = let open Evd in match evar_ident evk sigma with | None -> - str "?" ++ pr_id (pr_evar_suggested_name evk sigma) + str "?" ++ Id.print (pr_evar_suggested_name evk sigma) | Some id -> - str "?" ++ pr_id id + str "?" ++ Id.print id let pr_instance_status (sc,typ) = let open Evd in @@ -158,7 +158,7 @@ let pr_meta_map evd = let open Evd in let print_constr = print_kconstr in let pr_name = function - Name id -> str"[" ++ pr_id id ++ str"]" + Name id -> str"[" ++ Id.print id ++ str"]" | _ -> mt() in let pr_meta_binding = function | (mv,Cltyp (na,b)) -> @@ -178,23 +178,23 @@ let pr_decl (decl,ok) = let open NamedDecl in let print_constr = print_kconstr in match decl with - | LocalAssum (id,_) -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}") - | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ + | LocalAssum (id,_) -> if ok then Id.print id else (str "{" ++ Id.print id ++ str "}") + | LocalDef (id,c,_) -> str (if ok then "(" else "{") ++ Id.print id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") let pr_evar_source = function - | Evar_kinds.NamedHole id -> pr_id id + | Evar_kinds.NamedHole id -> Id.print id | Evar_kinds.QuestionMark _ -> str "underscore" | Evar_kinds.CasesType false -> str "pattern-matching return predicate" | Evar_kinds.CasesType true -> str "subterm of pattern-matching return predicate" - | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id + | Evar_kinds.BinderType (Name id) -> str "type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let open Globnames in let print_constr = print_kconstr in let id = Option.get ido in - str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ + str "parameter " ++ Id.print id ++ spc () ++ str "of" ++ spc () ++ print_constr (printable_constr_of_global c) | Evar_kinds.InternalHole -> str "internal placeholder" | Evar_kinds.TomatchTypeParameter (ind,n) -> @@ -203,7 +203,7 @@ let pr_evar_source = function | Evar_kinds.GoalEvar -> str "goal evar" | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> str "matching variable" - | Evar_kinds.VarInstance id -> str "instance of " ++ pr_id id + | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id | Evar_kinds.SubEvar evk -> let open Evd in str "subterm of " ++ str (string_of_existential evk) @@ -435,7 +435,7 @@ let pr_var_decl env decl = (str" := " ++ pb ++ cut () ) in let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in let ptyp = (str" : " ++ pt) in - (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp)) + (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp)) let pr_rel_decl env decl = let open RelDecl in @@ -449,7 +449,7 @@ let pr_rel_decl env decl = let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in match get_name decl with | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) - | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) + | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp) let print_named_context env = hv 0 (fold_named_context diff --git a/engine/uState.ml b/engine/uState.ml index 77837fefc..dfea25dd0 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -269,7 +269,7 @@ let universe_context ~names ~extensible ctx = try UNameMap.find (Id.to_string id) (fst ctx.uctx_names) with Not_found -> user_err ?loc ~hdr:"universe_context" - (str"Universe " ++ Nameops.pr_id id ++ str" is not bound anymore.") + (str"Universe " ++ Id.print id ++ str" is not bound anymore.") in (l :: newinst, Univ.LSet.remove l acc)) names ([], levels) in diff --git a/engine/universes.ml b/engine/universes.ml index 3136f805c..6c1b64d74 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -16,7 +16,7 @@ open Univ open Globnames let pr_with_global_universes l = - try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) + try Id.print (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l (** Local universe names of polymorphic references *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a0a749bfb..c4e0ac500 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -122,7 +122,7 @@ type internalization_error = exception InternalizationError of internalization_error Loc.located let explain_variable_capture id id' = - pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++ + Id.print id ++ str " is dependent in the type of " ++ Id.print id' ++ strbrk ": cannot interpret both of them with the same type" let explain_illegal_metavariable = @@ -132,12 +132,12 @@ let explain_not_a_constructor ref = str "Unknown constructor: " ++ pr_reference ref let explain_unbound_fix_name is_cofix id = - str "The name" ++ spc () ++ pr_id id ++ + str "The name" ++ spc () ++ Id.print id ++ spc () ++ str "is not bound in the corresponding" ++ spc () ++ str (if is_cofix then "co" else "") ++ str "fixpoint definition" let explain_non_linear_pattern id = - str "The variable " ++ pr_id id ++ str " is bound several times in pattern" + str "The variable " ++ Id.print id ++ str " is bound several times in pattern" let explain_bad_patterns_number n1 n2 = str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++ @@ -163,7 +163,7 @@ let error_parameter_not_implicit ?loc = "they must be replaced by '_'.") let error_ldots_var ?loc = - user_err ?loc (str "Special token " ++ pr_id ldots_var ++ + user_err ?loc (str "Special token " ++ Id.print ldots_var ++ str " is for use in the Notation command.") (**********************************************************************) @@ -263,13 +263,13 @@ let pr_scope_stack = function let error_inconsistent_scope ?loc id scopes1 scopes2 = user_err ?loc ~hdr:"set_var_scope" - (pr_id id ++ str " is here used in " ++ + (Id.print id ++ str " is here used in " ++ pr_scope_stack scopes2 ++ strbrk " while it was elsewhere used in " ++ pr_scope_stack scopes1) let error_expect_binder_notation_type ?loc id = user_err ?loc - (pr_id id ++ + (Id.print id ++ str " is expected to occur in binding position in the right-hand side.") let set_var_scope ?loc id istermvar env ntnvars = @@ -365,7 +365,7 @@ let check_hidden_implicit_parameters ?loc id impls = | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + user_err ?loc (Id.print id ++ strbrk " is already used as name of " ++ strbrk "a parameter of the inductive type; bound variables in " ++ strbrk "the type of a constructor shall use a different name.") @@ -743,7 +743,7 @@ let string_of_ty = function let gvar (loc, id) us = match us with | None -> DAst.make ?loc @@ GVar id | Some _ -> - user_err ?loc (str "Variable " ++ pr_id id ++ + user_err ?loc (str "Variable " ++ Id.print id ++ str " cannot have a universe instance") let intern_var genv (ltacvars,ntnvars) namedctx loc id us = @@ -772,7 +772,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us = else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err ?loc ~hdr:"intern_var" - (str "variable " ++ pr_id id ++ str " should be bound to a term.") + (str "variable " ++ Id.print id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) let _ = Context.Named.lookup id namedctx in @@ -1570,9 +1570,9 @@ let extract_explicit_arg imps args = | ExplByName id -> if not (exists_implicit_name id imps) then user_err ?loc - (str "Wrong argument name: " ++ pr_id id ++ str "."); + (str "Wrong argument name: " ++ Id.print id ++ str "."); if Id.Map.mem id eargs then - user_err ?loc (str "Argument name " ++ pr_id id + user_err ?loc (str "Argument name " ++ Id.print id ++ str " occurs more than once."); id | ExplByPos (p,_id) -> @@ -1990,7 +1990,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (let (id,(loc,_)) = Id.Map.choose eargs in user_err ?loc (str "Not enough non implicit \ arguments to accept the argument bound to " ++ - pr_id id ++ str".")); + Id.print id ++ str".")); [] | ([], rargs) -> assert (Id.Map.is_empty eargs); 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 () = diff --git a/interp/impargs.ml b/interp/impargs.ml index 72d22db4d..f70154e61 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -10,7 +10,6 @@ open CErrors open Util open Names open Globnames -open Nameops open Term open Constr open Reduction @@ -344,7 +343,7 @@ let check_correct_manual_implicits autoimps l = | ExplByName id,(b,fi,forced) -> if not forced then user_err - (str "Wrong or non-dependent implicit argument name: " ++ pr_id id ++ str ".") + (str "Wrong or non-dependent implicit argument name: " ++ Id.print id ++ str ".") | ExplByPos (i,_id),_t -> if i<1 || i>List.length autoimps then user_err diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cae67c3e7..a5302b54d 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -29,11 +29,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" let declare_generalizable_ident table (loc,id) = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id ++ str + ((Id.print id ++ str " is not declarable as generalizable identifier: it must have no trailing digits, quote, or _")); if Id.Pred.mem id table then user_err ?loc ~hdr:"declare_generalizable_ident" - ((pr_id id++str" is already declared as a generalizable identifier")) + ((Id.print id++str" is already declared as a generalizable identifier")) else Id.Pred.add id table let add_generalizable gen table = @@ -80,7 +80,7 @@ let is_freevar ids env x = let ungeneralizable loc id = user_err ?loc ~hdr:"Generalization" - (str "Unbound and ungeneralizable variable " ++ pr_id id) + (str "Unbound and ungeneralizable variable " ++ Id.print id) let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let found loc id bdvars l = @@ -152,7 +152,7 @@ let combine_params avoid fn applied needed = | Anonymous -> false in if not (List.exists is_id needed) then - user_err ?loc (str "Wrong argument name: " ++ Nameops.pr_id id); + user_err ?loc (str "Wrong argument name: " ++ Id.print id); true | _ -> false) applied in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 0967d21f0..0344dda97 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -239,7 +239,7 @@ let subtract_loc loc1 loc2 = let check_is_hole id t = match DAst.get t with GHole _ -> () | _ -> user_err ?loc:(loc_of_glob_constr t) - (strbrk "In recursive notation with binders, " ++ pr_id id ++ + (strbrk "In recursive notation with binders, " ++ Id.print id ++ strbrk " is expected to come without type.") let pair_equal eq1 eq2 (a,b) (a',b') = eq1 a a' && eq2 b b' @@ -400,7 +400,7 @@ let check_variables_and_reversibility 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 - user_err (pr_id x ++ + user_err (Id.print 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 @@ -419,8 +419,8 @@ let check_variables_and_reversibility 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 - user_err (strbrk "in the right-hand side, " ++ pr_id x ++ - str " and " ++ pr_id y ++ strbrk " should appear in " ++ str s ++ + user_err (strbrk "in the right-hand side, " ++ Id.print x ++ + str " and " ++ Id.print y ++ strbrk " should appear in " ++ str s ++ str " position as part of a recursive pattern.") in let check_type x typ = match typ with @@ -838,7 +838,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v | Name id' -> if Id.equal (rename_var (snd alp) id) id' then na' else raise No_match in let unify_pat p p' = - if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p' + if cases_pattern_eq (map_cases_pattern_name_left (Name.map (rename_var (snd alp))) p) p' then p' else raise No_match in let unify_term_binder c = DAst.(map (fun b' -> match DAst.get c, b' with diff --git a/interp/reserve.ml b/interp/reserve.ml index dc0f60dcf..6fd1d0b58 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -87,12 +87,12 @@ let in_reserved : Id.t * notation_constr -> obj = let declare_reserved_type_binding (loc,id) t = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_reserved_type" - ((pr_id id ++ str + ((Id.print id ++ str " is not reservable: it must have no trailing digits, quote, or _")); begin try let _ = Id.Map.find id !reserve_table in user_err ?loc ~hdr:"declare_reserved_type" - ((pr_id id++str" is already bound to a type")) + ((Id.print id++str" is already bound to a type")) with Not_found -> () end; add_anonymous_leaf (in_reserved (id,t)) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index 84c6f4ef3..98e507309 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -6,16 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open CErrors open Util open Pp +open CErrors open Names open Libnames -open Notation_term open Libobject open Lib -open Nameops open Nametab +open Notation_term (* Syntactic definitions. *) @@ -31,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 user_err ~hdr:"cache_syntax_constant" - (pr_id (basename sp) ++ str " already exists"); + (Id.print (basename sp) ++ str " already exists"); add_syntax_constant kn pat onlyparse; Nametab.push_syndef (Nametab.Until i) sp kn diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 7a3c83ff9..c64d3aa26 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -186,14 +186,14 @@ let split_at_annot bl na = | CLocalDef ((_,na),_,_) as x :: rest -> if Name.equal (Name id) na then user_err ?loc - (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.") + (Id.print id ++ str" must be a proper parameter and not a local definition.") else aux (x :: acc) rest | CLocalPattern (_,_) :: rest -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") | [] -> - user_err ?loc - (str "No parameter named " ++ Nameops.pr_id id ++ str".") + user_err ?loc + (str "No parameter named " ++ Id.print id ++ str".") in aux [] bl (* Used in correctness and interface *) diff --git a/library/lib.ml b/library/lib.ml index df9563e45..36292d367 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -9,6 +9,7 @@ open Pp open CErrors open Util +open Names open Libnames open Globnames open Nameops @@ -285,7 +286,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_module dir in if exists then - user_err ~hdr:"open_module" (pr_id id ++ str " already exists"); + user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); add_entry (make_oname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix @@ -296,7 +297,7 @@ let start_modtype = start_mod true None let error_still_opened string oname = let id = basename (fst oname) in user_err - (str "The " ++ str string ++ str " " ++ pr_id id ++ str " is still opened.") + (str "The " ++ str string ++ str " " ++ Id.print id ++ str " is still opened.") let end_mod is_type = let oname,fs = @@ -337,8 +338,8 @@ let start_compilation s mp = let open_blocks_message es = let open_block_name = function - | oname, OpenedSection _ -> str "section " ++ pr_id (basename (fst oname)) - | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ pr_id (basename (fst oname)) + | oname, OpenedSection _ -> str "section " ++ Id.print (basename (fst oname)) + | oname, OpenedModule (ty,_,_,_) -> str (module_kind ty) ++ spc () ++ Id.print (basename (fst oname)) | _ -> assert false in str "The " ++ pr_enum open_block_name es ++ spc () ++ str "need" ++ str (if List.length es == 1 then "s" else "") ++ str " to be closed." @@ -395,7 +396,7 @@ let find_opening_node id = let id' = basename (fst oname) in if not (Names.Id.equal id id') then user_err ~hdr:"Lib.find_opening_node" - (str "Last block to end has name " ++ pr_id id' ++ str "."); + (str "Last block to end has name " ++ Id.print id' ++ str "."); entry with Not_found -> user_err Pp.(str "There is nothing to end.") @@ -526,7 +527,7 @@ let open_section id = let dir = add_dirpath_suffix olddir id in let prefix = dir, (mp, add_dirpath_suffix oldsec id) in if Nametab.exists_section dir then - user_err ~hdr:"open_section" (pr_id id ++ str " already exists."); + user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:`No in add_entry (make_oname id) (OpenedSection (prefix, fs)); (*Pushed for the lifetime of the section: removed by unfrozing the summary*) diff --git a/library/library.ml b/library/library.ml index 840fe563a..99ef66699 100644 --- a/library/library.ml +++ b/library/library.ml @@ -617,7 +617,7 @@ let check_coq_overwriting p id = let is_empty = match l with [] -> true | _ -> false in if not !Flags.boot && not is_empty && Id.equal (List.last l) coq_root then user_err - (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ pr_id id ++ str "." ++ spc () ++ + (str "Cannot build module " ++ pr_dirpath p ++ str "." ++ Id.print id ++ str "." ++ spc () ++ str "it starts with prefix \"Coq\" which is reserved for the Coq library.") let start_library fo = diff --git a/library/nameops.mli b/library/nameops.mli index 26f300b61..60e5a90bb 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -90,33 +90,34 @@ module Name : sig end val out_name : Name.t -> Id.t -(** @deprecated Same as [Name.get_id] *) +[@@ocaml.deprecated "Same as [Name.get_id]"] val name_fold : (Id.t -> 'a -> 'a) -> Name.t -> 'a -> 'a -(** @deprecated Same as [Name.fold_right] *) +[@@ocaml.deprecated "Same as [Name.fold_right]"] val name_iter : (Id.t -> unit) -> Name.t -> unit -(** @deprecated Same as [Name.iter] *) +[@@ocaml.deprecated "Same as [Name.iter]"] val name_app : (Id.t -> Id.t) -> Name.t -> Name.t -(** @deprecated Same as [Name.map] *) +[@@ocaml.deprecated "Same as [Name.map]"] val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t -(** @deprecated Same as [Name.fold_left_map] *) +[@@ocaml.deprecated "Same as [Name.fold_left_map]"] val name_max : Name.t -> Name.t -> Name.t -(** @deprecated Same as [Name.pick] *) +[@@ocaml.deprecated "Same as [Name.pick]"] val name_cons : Name.t -> Id.t list -> Id.t list -(** @deprecated Same as [Name.cons] *) +[@@ocaml.deprecated "Same as [Name.cons]"] val pr_name : Name.t -> Pp.t -(** @deprecated Same as [Name.print] *) +[@@ocaml.deprecated "Same as [Name.print]"] val pr_id : Id.t -> Pp.t -(** @deprecated Same as [Names.Id.print] *) +[@@ocaml.deprecated "Same as [Names.Id.print]"] val pr_lab : Label.t -> Pp.t +[@@ocaml.deprecated "Same as [Names.Label.print]"] (** some preset paths *) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 705a51edd..c63492d1b 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -6,10 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open Pp open CErrors open Util +open Names open Nameops open Namegen open Constr @@ -1143,7 +1143,7 @@ let subterm all flags (s : 'a pure_strategy) : 'a pure_strategy = (* | _ -> b') *) | Lambda (n, t, b) when flags.under_lambdas -> - let n' = name_app (fun id -> Tactics.fresh_id_in_env unfresh id env) n in + let n' = Nameops.Name.map (fun id -> Tactics.fresh_id_in_env unfresh id env) n in let open Context.Rel.Declaration in let env' = EConstr.push_rel (LocalAssum (n', t)) env in let bty = Retyping.get_type_of env' (goalevars evars) b in diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index b7b76c830..3a9179813 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -12,7 +12,6 @@ open CErrors open Util open Names open Globnames -open Nameops open Termops open Reductionops open Term @@ -55,7 +54,7 @@ exception PatternMatchingFailure let warn_meta_collision = CWarnings.create ~name:"meta-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variable " ++ pr_id name ++ + strbrk "Collision between bound variable " ++ Id.print name ++ strbrk " and a metavariable of same name.") diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 9e7652da6..fd6bfe0a2 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -12,7 +12,6 @@ open CErrors open Names open Locus open EConstr -open Nameops open Termops open Pretype_errors @@ -30,7 +29,7 @@ let explain_invalid_occurrence l = ++ prlist_with_sep spc int l ++ str "." let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." + Id.print id ++ str " has no value." let explain_occurrence_error = function | InvalidOccurrence l -> explain_invalid_occurrence l diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 055fd68f6..093f1f0b6 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -290,7 +290,7 @@ let warn_variable_collision = let open Pp in CWarnings.create ~name:"variable-collision" ~category:"ltac" (fun name -> - strbrk "Collision between bound variables of name " ++ pr_id name) + strbrk "Collision between bound variables of name " ++ Id.print name) let add_and_check_ident id set = if Id.Set.mem id set then warn_variable_collision id; @@ -524,7 +524,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function try Name (Id.Map.find id ltac_idents) with Not_found -> if Id.Map.mem id ltac_genargs then - user_err (str"Ltac variable"++spc()++ pr_id id ++ + user_err (str"Ltac variable"++spc()++ Id.print id ++ spc()++str"is not bound to an identifier."++spc()++ str"It cannot be used in a binder.") else n diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 48b33e708..b7b5b1662 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -616,7 +616,7 @@ let lookup_eliminator ind_sp s = with Not_found -> user_err ~hdr:"default_elim" (strbrk "Cannot find the elimination combinator " ++ - pr_id id ++ strbrk ", the elimination of the inductive definition " ++ + Id.print id ++ strbrk ", the elimination of the inductive definition " ++ pr_global_env Id.Set.empty (IndRef ind_sp) ++ strbrk " on sort " ++ Termops.pr_sort_family s ++ strbrk " is probably not allowed.") diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index ee79b5474..4d8c09c50 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -230,8 +230,8 @@ let error_instantiate_pattern id l = | [_] -> "is" | _ -> "are" in - user_err (str "Cannot substitute the term bound to " ++ pr_id id - ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l + user_err (str "Cannot substitute the term bound to " ++ Id.print id + ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") let instantiate_pattern env sigma lvar c = diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index b2b583ba7..e3470b0f1 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -382,9 +382,9 @@ let check_instance loc subst = function | [] -> () | (id,_) :: _ -> if List.mem_assoc id subst then - user_err ?loc (pr_id id ++ str "appears more than once.") + user_err ?loc (Id.print id ++ str "appears more than once.") else - user_err ?loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".") + user_err ?loc (str "No such variable in the signature of the existential variable: " ++ Id.print id ++ str ".") (* used to enforce a name in Lambda when the type constraints itself is named, hence possibly dependent *) @@ -410,8 +410,8 @@ let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in try mkRel (pi1 (lookup_rel_id id' (rel_context env))) with Not_found -> - user_err (str "Ltac variable " ++ pr_id id0 ++ - str " depends on pattern variable name " ++ pr_id id ++ + user_err (str "Ltac variable " ++ Id.print id0 ++ + str " depends on pattern variable name " ++ Id.print id ++ str " which is not bound in current context.") let protected_get_type_of env sigma c = @@ -454,7 +454,7 @@ let pretype_id pretype k0 loc env evdref lvar id = if Id.Map.mem id lvar.ltac_genargs then begin let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in user_err ?loc - (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \ + (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \ bound to a " ++ Geninterp.Val.pr typ ++ str ".") end; (* Check if [id] is a section or goal variable *) @@ -1089,7 +1089,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update = with Not_found -> user_err ?loc (str "Cannot interpret " ++ pr_existential_key !evdref evk ++ - str " in current context: no binding for " ++ pr_id id ++ str ".") in + str " in current context: no binding for " ++ Id.print id ++ str ".") in ((id,c)::subst, update) in let subst,inst = List.fold_right f hyps ([],update) in check_instance loc subst inst; diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cb24ca804..e6d8a0af2 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -300,7 +300,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) let error_not_structure ref = user_err ~hdr:"object_declare" - (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.") + (Id.print (basename_of_global ref) ++ str" is not a structure object.") let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5eb6b780a..a4e2f90d4 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1628,7 +1628,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = if name == Anonymous then next_ident_away_in_goal x ids else if mem_named_context_val x (named_context_val env) then user_err ~hdr:"Unification.make_abstraction_core" - (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.") + (str "The variable " ++ Id.print x ++ str " is already declared.") else x in diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index d7c42d03a..5576e33f4 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -6,10 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names -open Nameops -open CErrors open Pp +open CErrors +open Names (** Local universes and constraints declarations *) type universe_decl = @@ -34,7 +33,7 @@ let interp_univ_constraints env evd cstrs = | GType (Some (loc, Name id)) -> try loc, Evd.universe_of_name evd (Id.to_string id) with Not_found -> - user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id) + user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id) in let interp (evd,cstrs) (u, d, u') = let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 109a40a03..0f6452de6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -171,17 +171,17 @@ let tag_var = tag Tag.variable let pr_qualid sp = let (sl, id) = repr_qualid sp in - let id = tag_ref (pr_id id) in + let id = tag_ref (Id.print id) in let sl = match List.rev (DirPath.repr sl) with | [] -> mt () | sl -> - let pr dir = tag_path (pr_id dir) ++ str "." in + let pr dir = tag_path (Id.print dir) ++ str "." in prlist pr sl in sl ++ id - let pr_id = pr_id - let pr_name = pr_name + let pr_id = Id.print + let pr_name = Name.print let pr_qualid = pr_qualid let pr_patvar = pr_id diff --git a/printing/pputils.ml b/printing/pputils.ml index 9ef9162ae..3cc7a3e6b 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -9,7 +9,6 @@ open Util open Pp open Genarg -open Nameops open Misctypes open Locus open Genredexpr @@ -27,7 +26,7 @@ let pr_located pr (loc, x) = let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (_,s) -> pr_id s + | ArgVar (_,s) -> Names.Id.print s let pr_with_occurrences pr keyword (occs,c) = match occs with diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f69c4bce7..acbd2d5d2 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -94,7 +94,7 @@ let print_ref reduce ref = (********************************) (** Printing implicit arguments *) -let pr_impl_name imp = pr_id (name_of_implicit imp) +let pr_impl_name imp = Id.print (name_of_implicit imp) let print_impargs_by_name max = function | [] -> [] @@ -238,7 +238,7 @@ let print_primitive_record recflag mipv = function | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] + [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] let print_primitive ref = @@ -271,7 +271,7 @@ let print_name_infos ref = let print_id_args_data test pr id l = if List.exists test l then - pr (str "For " ++ pr_id id) l + pr (str "For " ++ Id.print id) l else [] @@ -456,7 +456,7 @@ let print_located_qualid name flags ref = | [] -> let (dir,id) = repr_qualid qid in if DirPath.is_empty dir then - str "No " ++ str name ++ str " of basename" ++ spc () ++ pr_id id + str "No " ++ str name ++ str " of basename" ++ spc () ++ Id.print id else str "No " ++ str name ++ str " of suffix" ++ spc () ++ pr_qualid qid | l -> @@ -608,7 +608,7 @@ let gallina_print_syntactic_def kn = hov 2 (hov 4 (str "Notation " ++ pr_qualid qid ++ - prlist (fun id -> spc () ++ pr_id id) (List.map fst vars) ++ + prlist (fun id -> spc () ++ Id.print id) (List.map fst vars) ++ spc () ++ str ":=") ++ spc () ++ Constrextern.without_specific_symbols @@ -638,7 +638,7 @@ let gallina_print_leaf_entry with_values ((sp,kn as oname),lobj) = | (_,s) -> None let gallina_print_library_entry with_values ent = - let pr_name (sp,_) = pr_id (basename sp) in + let pr_name (sp,_) = Id.print (basename sp) in match ent with | (oname,Lib.Leaf lobj) -> gallina_print_leaf_entry with_values (oname,lobj) diff --git a/printing/printer.ml b/printing/printer.ml index 751e91cf0..075b03b7d 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -478,7 +478,7 @@ let pr_predicate pr_elt (b, elts) = if List.is_empty elts then str"none" else pr_elts let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) -let pr_idpred p = pr_predicate Nameops.pr_id (Id.Pred.elements p) +let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) let pr_transparent_state (ids, csts) = hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ diff --git a/printing/printmod.ml b/printing/printmod.ml index 6b3b177aa..0abca0160 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -12,7 +12,6 @@ open Pp open Names open Environ open Declarations -open Nameops open Globnames open Libnames open Goptions @@ -80,7 +79,7 @@ let print_params env sigma params = let print_constructors envpar sigma names types = let pc = prlist_with_sep (fun () -> brk(1,0) ++ str "| ") - (fun (id,c) -> pr_id id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) + (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c) (Array.to_list (Array.map2 (fun n t -> (n,t)) names types)) in hv 0 (str " " ++ pc) @@ -107,7 +106,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) = else mt () in hov 0 ( - pr_id mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ + Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes @@ -189,15 +188,15 @@ let print_record env mind mib = Printer.pr_cumulative (Declareops.inductive_is_polymorphic mib) (Declareops.inductive_is_cumulative mib) ++ - def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ + def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ - str ":= " ++ pr_id mip.mind_consnames.(0)) ++ + str ":= " ++ Id.print mip.mind_consnames.(0)) ++ brk(1,2) ++ hv 2 (str "{ " ++ prlist_with_sep (fun () -> str ";" ++ brk(2,0)) (fun (id,b,c) -> - pr_id id ++ str (if b then " : " else " := ") ++ + Id.print id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" @@ -215,9 +214,9 @@ let pr_mutual_inductive_body env mind mib = (** Modpaths *) let rec print_local_modpath locals = function - | MPbound mbid -> pr_id (Util.List.assoc_f MBId.equal mbid locals) + | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals) | MPdot(mp,l) -> - print_local_modpath locals mp ++ str "." ++ pr_lab l + print_local_modpath locals mp ++ str "." ++ Label.print l | MPfile _ -> raise Not_found let print_modpath locals mp = @@ -403,7 +402,7 @@ let rec print_functor fty fatom is_type env mp locals = function let kwd = if is_type then "Funsig" else "Functor" in hov 2 (keyword kwd ++ spc () ++ - str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++ + str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++ spc() ++ print_functor fty fatom is_type env' mp locals' me2) let rec print_expression x = diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 5ef7fac81..16798a1d5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -154,7 +154,7 @@ let error_incompatible_inst clenv mv = Name id -> user_err ~hdr:"clenv_assign" (str "An incompatible instantiation has already been found for " ++ - pr_id id) + Id.print id) | _ -> anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.") @@ -417,7 +417,7 @@ let check_bindings bl = match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with | NamedHyp s :: _ -> user_err - (str "The variable " ++ pr_id s ++ + (str "The variable " ++ Id.print s ++ str " occurs more than once in binding list."); | AnonHyp n :: _ -> user_err @@ -435,12 +435,12 @@ let explain_no_such_bound_variable evd id = in let mvl = List.fold_left fold [] (Evd.meta_list evd) in user_err ~hdr:"Evd.meta_with_name" - (str"No such bound variable " ++ pr_id id ++ + (str"No such bound variable " ++ Id.print id ++ (if mvl == [] then str " (no bound variables at all in the expression)." else (str" (possible name" ++ str (if List.length mvl == 1 then " is: " else "s are: ") ++ - pr_enum pr_id mvl ++ str")."))) + pr_enum Id.print mvl ++ str")."))) let meta_with_name evd id = let na = Name id in @@ -460,7 +460,7 @@ let meta_with_name evd id = n | _ -> user_err ~hdr:"Evd.meta_with_name" - (str "Binder name \"" ++ pr_id id ++ + (str "Binder name \"" ++ Id.print id ++ strbrk "\" occurs more than once in clause.") let meta_of_binder clause loc mvs = function @@ -474,7 +474,7 @@ let error_already_defined b = match b with | NamedHyp id -> user_err - (str "Binder name \"" ++ pr_id id ++ + (str "Binder name \"" ++ Id.print id ++ str"\" already defined with incompatible value.") | AnonHyp n -> anomaly @@ -639,10 +639,10 @@ let explain_no_such_bound_variable holes id = let mvl = List.fold_right fold holes [] in let expl = match mvl with | [] -> str " (no bound variables at all in the expression)." - | [id] -> str "(possible name is: " ++ pr_id id ++ str ")." - | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")." + | [id] -> str "(possible name is: " ++ Id.print id ++ str ")." + | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")." in - user_err (str "No such bound variable " ++ pr_id id ++ expl) + user_err (str "No such bound variable " ++ Id.print id ++ expl) let evar_with_name holes id = let map h = match h.hole_name with @@ -655,7 +655,7 @@ let evar_with_name holes id = | [h] -> h.hole_evar | _ -> user_err - (str "Binder name \"" ++ pr_id id ++ + (str "Binder name \"" ++ Id.print id ++ str "\" occurs more than once in clause.") let evar_of_binder holes = function diff --git a/proofs/logic.ml b/proofs/logic.ml index a633238f4..13a4e4ce3 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -140,9 +140,9 @@ let reorder_context env sigma sign ord = let ((d,h),mh) = find_q top moved_hyps in if occur_vars_in_decl env sigma h d then user_err ~hdr:"reorder_context" - (str "Cannot move declaration " ++ pr_id top ++ spc() ++ + (str "Cannot move declaration " ++ Id.print top ++ spc() ++ str "before " ++ - pr_sequence pr_id + pr_sequence Id.print (Id.Set.elements (Id.Set.inter h (global_vars_set_of_decl env sigma d)))); step ord' expected ctxt_head mh (d::ctxt_tail) @@ -173,7 +173,7 @@ let check_decl_position env sigma sign d = let deps = dependency_closure env sigma (named_context_of_val sign) needed in if Id.List.mem x deps then user_err ~hdr:"Logic.check_decl_position" - (str "Cannot create self-referring hypothesis " ++ pr_id x); + (str "Cannot create self-referring hypothesis " ++ Id.print x); x::deps (* Auxiliary functions for primitive MOVE tactic @@ -234,10 +234,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto = if not (move_location_eq hto (MoveAfter hyp)) then (first, d::middle) else - user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++ - Miscprint.pr_move_location pr_id hto ++ + user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++ + Miscprint.pr_move_location Id.print hto ++ str (if toleft then ": it occurs in the type of " else ": it depends on ") - ++ pr_id hyp ++ str ".") + ++ Id.print hyp ++ str ".") else (d::first, middle) in @@ -507,10 +507,10 @@ let convert_hyp check sign sigma d = let env = Global.env_of_context sign in if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the type of " ++ pr_id id ++ str "."); + (str "Incorrect change of the type of " ++ Id.print id ++ str "."); if check && not (Option.equal (is_conv env sigma) b c) then user_err ~hdr:"Logic.convert_hyp" - (str "Incorrect change of the body of "++ pr_id id ++ str "."); + (str "Incorrect change of the body of "++ Id.print id ++ str "."); if check then reorder := check_decl_position env sigma sign d; map_named_decl EConstr.Unsafe.to_constr d) in reorder_val_context env sigma sign' !reorder diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml index 5d37c8a02..92b58b409 100644 --- a/proofs/miscprint.ml +++ b/proofs/miscprint.ml @@ -6,8 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Misctypes open Pp +open Names +open Misctypes (** Printing of [intro_pattern] *) @@ -18,8 +19,8 @@ let rec pr_intro_pattern prc (_,pat) = match pat with | IntroAction p -> pr_intro_pattern_action prc p and pr_intro_pattern_naming = function - | IntroIdentifier id -> Nameops.pr_id id - | IntroFresh id -> str "?" ++ Nameops.pr_id id + | IntroIdentifier id -> Id.print id + | IntroFresh id -> str "?" ++ Id.print id | IntroAnonymous -> str "?" and pr_intro_pattern_action prc = function diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 97faa1684..8b788bb38 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -185,7 +185,7 @@ let msg_proofs () = match get_all_proof_names () with | [] -> (spc () ++ str"(No proof-editing in progress).") | l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++ - (pr_sequence Nameops.pr_id l) ++ str".") + (pr_sequence Id.print l) ++ str".") let there_is_a_proof () = not (List.is_empty !pstates) let there_are_pending_proofs () = there_is_a_proof () diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 9097aebd0..7eae2541e 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Nameops open Term open Termops open EConstr @@ -261,7 +260,7 @@ module SearchProblem = struct let g = find_first_goal lg in let hyps = pf_ids_of_hyps g in let secvars = secvars_of_hyps (pf_hyps g) in - let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ pr_id id)) in + let map_assum id = (e_give_exact (mkVar id), (-1), lazy (str "exact" ++ spc () ++ Id.print id)) in let assumption_tacs = let tacs = List.map map_assum hyps in let l = filter_tactics s.tacres tacs in diff --git a/tactics/equality.ml b/tactics/equality.ml index 881000219..7b2445ff5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1760,7 +1760,7 @@ let subst_one_var dep_proof_ok x = let test hyp _ = is_eq_x gl x hyp in Context.Named.fold_outside test ~init:() hyps; user_err ~hdr:"Subst" - (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in subst_one dep_proof_ok x res diff --git a/tactics/inv.ml b/tactics/inv.ml index c5aa74ba5..8648dfb90 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -10,7 +10,6 @@ open Pp open CErrors open Util open Names -open Nameops open Term open Termops open EConstr @@ -78,7 +77,7 @@ let make_inv_predicate env evd indf realargs id status concl = | Dep dflt_concl -> if not (occur_var env !evd id concl) then user_err ~hdr:"make_inv_predicate" - (str "Current goal does not depend on " ++ pr_id id ++ str"."); + (str "Current goal does not depend on " ++ Id.print id ++ str"."); (* We abstract the conclusion of goal with respect to realargs and c to * be concl in order to rewrite and have c also rewritten when the case * will be done *) @@ -442,7 +441,7 @@ let raw_inversion inv_kind id status names = let (ind, t) = try pf_apply Tacred.reduce_to_atomic_ind gl (pf_unsafe_type_of gl c) with UserError _ -> - let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in + let msg = str "The type of " ++ Id.print id ++ str " is not inductive." in CErrors.user_err msg in let IndType (indf,realargs) = find_rectype env sigma t in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ba244a794..096274c68 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -181,7 +181,7 @@ let introduction ?(check=true) id = let env = Proofview.Goal.env gl in let () = if check && mem_named_context_val id hyps then user_err ~hdr:"Tactics.introduction" - (str "Variable " ++ pr_id id ++ str " is already declared.") + (str "Variable " ++ Id.print id ++ str " is already declared.") in let open Context.Named.Declaration in match EConstr.kind sigma concl with @@ -244,11 +244,11 @@ let convert_leq x y = convert_gen Reduction.CUMUL x y let clear_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> - pr_id id ++ str " is used in conclusion." + Id.print id ++ str " is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str"." + Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> - str "Cannot remove " ++ pr_id id ++ + str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." @@ -257,12 +257,12 @@ let error_clear_dependency env sigma id err = let replacing_dependency_msg env sigma id = function | Evarutil.OccurHypInSimpleClause None -> - str "Cannot change " ++ pr_id id ++ str ", it is used in conclusion." + str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - str "Cannot change " ++ pr_id id ++ - strbrk ", it is used in hypothesis " ++ pr_id id' ++ str"." + str "Cannot change " ++ Id.print id ++ + strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> - str "Cannot change " ++ pr_id id ++ + str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." @@ -360,7 +360,7 @@ let rename_hyp repl = let () = try let elt = Id.Set.choose (Id.Set.inter dst mods) in - CErrors.user_err (pr_id elt ++ str " is already used") + CErrors.user_err (Id.print elt ++ str " is already used") with Not_found -> () in (** All is well *) @@ -435,7 +435,7 @@ let find_name mayrepl decl naming gl = match naming with let ids_of_hyps = Tacmach.New.pf_ids_set_of_hyps gl in let id' = next_ident_away id ids_of_hyps in if not mayrepl && not (Id.equal id' id) then - user_err ?loc (pr_id id ++ str" is already used."); + user_err ?loc (Id.print id ++ str" is already used."); id (**************************************************************) @@ -489,7 +489,7 @@ let internal_cut_gen ?(check=true) dir replace id t = sign',t,concl,sigma else (if check && mem_named_context_val id sign then - user_err (str "Variable " ++ pr_id id ++ str " is already declared."); + user_err (str "Variable " ++ Id.print id ++ str " is already declared."); push_named_context_val (LocalAssum (id,t)) sign,t,concl,sigma) in let nf_t = nf_betaiota sigma t in Proofview.tclTHEN @@ -585,7 +585,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" - (str "Name " ++ pr_id f ++ str " already used in the environment"); + (str "Name " ++ Id.print f ++ str " already used in the environment"); mk_sign (push_named_context_val (LocalAssum (f, ar)) sign) oth in let nenv = reset_with_named_context (mk_sign (named_context_val env) all) env in @@ -675,7 +675,7 @@ let pf_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); LocalAssum (id,redfun' ty) | LocalDef (id,b,ty) -> let b' = if where != InHypTypeOnly then redfun' b else b in @@ -776,7 +776,7 @@ let pf_e_reduce_decl redfun where decl gl = match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); let (sigma, ty') = redfun sigma ty in (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> @@ -819,7 +819,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm match decl with | LocalAssum (id,ty) -> if where == InHypValueOnly then - user_err (pr_id id ++ str " has no value."); + user_err (Id.print id ++ str " has no value."); let (sigma, ty') = redfun false env sigma ty in (sigma, LocalAssum (id, ty')) | LocalDef (id,b,ty) -> @@ -1133,7 +1133,7 @@ let is_quantified_hypothesis id gl = let msg_quantified_hypothesis = function | NamedHyp id -> - str "quantified hypothesis named " ++ pr_id id + str "quantified hypothesis named " ++ Id.print id | AnonHyp n -> pr_nth n ++ str " non dependent hypothesis" @@ -1284,7 +1284,7 @@ let error_uninstantiated_metas t clenv = let t = EConstr.Unsafe.to_constr t in let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in let id = match na with Name id -> id | _ -> anomaly (Pp.str "unnamed dependent meta.") - in user_err (str "Cannot find an instance for " ++ pr_id id ++ str".") + in user_err (str "Cannot find an instance for " ++ Id.print id ++ str".") let check_unresolved_evars_of_metas sigma clenv = (* This checks that Metas turned into Evars by *) @@ -1593,7 +1593,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) let new_hyp_typ = clenv_type elimclause'' in if EConstr.eq_constr sigma hyp_typ new_hyp_typ then user_err ~hdr:"general_rewrite_in" - (str "Nothing to rewrite in " ++ pr_id id ++ str"."); + (str "Nothing to rewrite in " ++ Id.print id ++ str"."); clenv_refine_in with_evars id id sigma elimclause'' (fun id -> Proofview.tclUNIT ()) end @@ -2046,8 +2046,8 @@ let assumption = let on_the_bodies = function | [] -> assert false -| [id] -> str " depends on the body of " ++ pr_id id -| l -> str " depends on the bodies of " ++ pr_sequence pr_id l +| [id] -> str " depends on the body of " ++ Id.print id +| l -> str " depends on the bodies of " ++ pr_sequence Id.print l exception DependsOnBody of Id.t option @@ -2084,7 +2084,7 @@ let clear_body ids = let map = function | LocalAssum (id,t) as decl -> let () = if List.mem_f Id.equal id ids then - user_err (str "Hypothesis " ++ pr_id id ++ str " is not a local definition") + user_err (str "Hypothesis " ++ Id.print id ++ str " is not a local definition") in decl | LocalDef (id,_,t) as decl -> @@ -2116,7 +2116,7 @@ let clear_body ids = with DependsOnBody where -> let msg = match where with | None -> str "Conclusion" ++ on_the_bodies ids - | Some id -> str "Hypothesis " ++ pr_id id ++ on_the_bodies ids + | Some id -> str "Hypothesis " ++ Id.print id ++ on_the_bodies ids in Tacticals.New.tclZEROMSG msg in @@ -2419,10 +2419,10 @@ let rec check_name_unicity env ok seen = function | (loc, IntroNaming (IntroIdentifier id)) :: l -> (try ignore (if List.mem_f Id.equal id ok then raise Not_found else lookup_named id env); - user_err ?loc (pr_id id ++ str" is already used.") + user_err ?loc (Id.print id ++ str" is already used.") with Not_found -> if List.mem_f Id.equal id seen then - user_err ?loc (pr_id id ++ str" is used twice.") + user_err ?loc (Id.print id ++ str" is used twice.") else check_name_unicity env ok (id::seen) l) | (_, IntroAction (IntroOrAndPattern l)) :: l' -> @@ -2743,7 +2743,7 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty = | IntroFresh heq_base -> fresh_id_in_env (Id.Set.singleton id) heq_base env | IntroIdentifier id -> if List.mem id (ids_of_named_context (named_context env)) then - user_err ?loc (pr_id id ++ str" is already used."); + user_err ?loc (Id.print id ++ str" is already used."); id in let eqdata = build_coq_eq_data () in let args = if lr then [t;mkVar id;c] else [t;c;mkVar id]in @@ -2826,7 +2826,7 @@ let enough_by na t tac = forward false (Some (Some tac)) (ipat_of_name na) t let generalized_name env sigma c t ids cl = function | Name id as na -> if Id.List.mem id ids then - user_err (pr_id id ++ str " is already used."); + user_err (Id.print id ++ str " is already used."); na | Anonymous -> match EConstr.kind sigma c with @@ -3076,7 +3076,7 @@ let unfold_body x = let env = Proofview.Goal.env (Proofview.Goal.assume gl) in let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" - (pr_id x ++ str" is not a defined hypothesis.") + (Id.print x ++ str" is not a defined hypothesis.") | LocalDef (_,xval,_) -> xval in let xval = EConstr.of_constr xval in @@ -3913,7 +3913,7 @@ let specialize_eqs id = (internal_cut true id ty') (exact_no_check ((* refresh_universes_strict *) acc')) else - Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ pr_id id) + Tacticals.New.tclFAIL 0 (str "Nothing to do in hypothesis " ++ Id.print id) end let specialize_eqs id = Proofview.Goal.enter begin fun gl -> @@ -4369,7 +4369,7 @@ let clear_unselected_context id inhyps cls = if occur_var (Tacmach.New.pf_env gl) (Tacmach.New.project gl) id (Tacmach.New.pf_concl gl) && cls.concl_occs == NoOccurrences then user_err - (str "Conclusion must be mentioned: it depends on " ++ pr_id id + (str "Conclusion must be mentioned: it depends on " ++ Id.print id ++ str "."); match cls.onhyps with | Some hyps -> diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 3cf181441..9e63df51d 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -19,7 +19,6 @@ open Termops open Declarations open Names open Globnames -open Nameops open Inductiveops open Tactics open Ind_tables @@ -361,7 +360,7 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) else user_err ~hdr:"AutoIndDecl.do_replace_lb" - (str "Var " ++ pr_id s ++ str " seems unknown.") + (str "Var " ++ Id.print s ++ str " seems unknown.") ) in mkVar (find 1) with e when CErrors.noncritical e -> @@ -422,7 +421,7 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = if Id.equal avoid.(n-i) s then avoid.(n-i-x) else (if i<n then find (i+1) else user_err ~hdr:"AutoIndDecl.do_replace_bl" - (str "Var " ++ pr_id s ++ str " seems unknown.") + (str "Var " ++ Id.print s ++ str " seems unknown.") ) in mkVar (find 1) with e when CErrors.noncritical e -> diff --git a/vernac/classes.ml b/vernac/classes.ml index 22117f7e1..20cb43b24 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -180,7 +180,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) Name id -> let sp = Lib.make_path id in if Nametab.exists_cci sp then - user_err ~hdr:"new_instance" (Nameops.pr_id id ++ Pp.str " already exists."); + user_err ~hdr:"new_instance" (Id.print id ++ Pp.str " already exists."); id | Anonymous -> let i = Nameops.add_suffix (id_of_class k) "_instance_0" in diff --git a/vernac/command.ml b/vernac/command.ml index db3fa1955..be54f97b7 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -60,7 +60,7 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function if not has_no_args then user_err ?loc (strbrk"Cannot infer the non constant arguments of the conclusion of " - ++ pr_id cs ++ str "."); + ++ Id.print cs ++ str "."); let args = List.map (fun id -> CAst.make ?loc @@ CRef(Ident(loc,id),None)) params in CAppExpl ((None,Ident(loc,name),None),List.rev args) | c -> c @@ -181,7 +181,7 @@ match local with let () = assumption_message ident in let () = if not !Flags.quiet && Proof_global.there_are_pending_proofs () then - Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++ + Feedback.msg_info (str"Variable" ++ spc () ++ Id.print ident ++ strbrk " is not visible from current goals") in let r = VarRef ident in @@ -328,9 +328,9 @@ type structured_inductive_expr = let minductive_message warn = function | [] -> user_err Pp.(str "No inductive definition.") - | [x] -> (pr_id x ++ str " is defined" ++ + | [x] -> (Id.print x ++ str " is defined" ++ if warn then str " as a non-primitive record" else 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 defined") let check_all_names_different indl = @@ -764,11 +764,11 @@ let rec partial_order cmp = function let non_full_mutual_message x xge y yge isfix rest = let reason = if Id.List.mem x yge then - pr_id y ++ str " depends on " ++ pr_id x ++ strbrk " but not conversely" + Id.print y ++ str " depends on " ++ Id.print x ++ strbrk " but not conversely" else if Id.List.mem y xge then - pr_id x ++ str " depends on " ++ pr_id y ++ strbrk " but not conversely" + Id.print x ++ str " depends on " ++ Id.print y ++ strbrk " but not conversely" else - pr_id y ++ str " and " ++ pr_id x ++ strbrk " are not mutually dependent" in + Id.print y ++ str " and " ++ Id.print x ++ strbrk " are not mutually dependent" in let e = if List.is_empty rest then reason else strbrk "e.g., " ++ reason in let k = if isfix then "fixpoint" else "cofixpoint" in let w = diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index d7a4fcca3..c18744052 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -11,18 +11,17 @@ open Declare open Entries open Globnames open Impargs -open Nameops let warn_definition_not_visible = CWarnings.create ~name:"definition-not-visible" ~category:"implicits" Pp.(fun ident -> strbrk "Section definition " ++ - pr_id ident ++ strbrk " is not visible from current goals") + Names.Id.print ident ++ strbrk " is not visible from current goals") let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" Pp.(fun (id,kind) -> - pr_id id ++ strbrk " is declared as a local " ++ str kind) + Names.Id.print id ++ strbrk " is declared as a local " ++ str kind) let get_locality id ~kind = function | Discharge -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 7b1a948ed..d15a811ba 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -159,7 +159,7 @@ let pr_explicit env sigma t1 t2 = let pr_db env i = try match env |> lookup_rel i |> get_name with - | Name id -> pr_id id + | Name id -> Id.print id | Anonymous -> str "<>" with Not_found -> str "UNBOUND_REL_" ++ int i @@ -169,7 +169,7 @@ let explain_unbound_rel env sigma n = str "The reference " ++ int n ++ str " is free." let explain_unbound_var env v = - let var = pr_id v in + let var = Id.print v in str "No such section variable or assumption: " ++ var ++ str "." let explain_not_type env sigma j = @@ -189,7 +189,7 @@ let explain_bad_assumption env sigma j = let explain_reference_variables sigma id c = (* c is intended to be a global reference *) let pc = pr_global (fst (Termops.global_of_constr sigma c)) in - pc ++ strbrk " depends on the variable " ++ pr_id id ++ + pc ++ strbrk " depends on the variable " ++ Id.print id ++ strbrk " which is not declared in the context." let rec pr_disjunction pr = function @@ -415,7 +415,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let pr_lconstr_env env sigma c = pr_leconstr_env env sigma c in let prt_name i = match names.(i) with - Name id -> str "Recursive definition of " ++ pr_id id + Name id -> str "Recursive definition of " ++ Id.print id | Anonymous -> str "The " ++ pr_nth i ++ str " definition" in let st = match err with @@ -430,7 +430,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = let arg_env = make_all_name_different arg_env sigma in let called = match names.(j) with - Name id -> pr_id id + Name id -> Id.print id | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in let pr_db x = quote (pr_db env x) in let vars = @@ -450,7 +450,7 @@ let explain_ill_formed_rec_body env sigma err names i fixenv vdefj = | NotEnoughArgumentsForFixCall j -> let called = match names.(j) with - Name id -> pr_id id + Name id -> Id.print id | Anonymous -> str "the " ++ pr_nth i ++ str " definition" in str "Recursive call to " ++ called ++ str " has not enough arguments" @@ -528,7 +528,7 @@ let pr_trailing_ne_context_of env sigma = let rec explain_evar_kind env sigma evk ty = function | Evar_kinds.NamedHole id -> - strbrk "the existential variable named " ++ pr_id id + strbrk "the existential variable named " ++ Id.print id | Evar_kinds.QuestionMark _ -> strbrk "this placeholder of type " ++ ty | Evar_kinds.CasesType false -> @@ -537,12 +537,12 @@ let rec explain_evar_kind env sigma evk ty = function strbrk "a subterm of type " ++ ty ++ strbrk " in the type of this pattern-matching problem" | Evar_kinds.BinderType (Name id) -> - strbrk "the type of " ++ Nameops.pr_id id + strbrk "the type of " ++ Id.print id | Evar_kinds.BinderType Anonymous -> strbrk "the type of this anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in - strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ + strbrk "the implicit parameter " ++ Id.print id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Id.Set.empty c ++ strbrk " whose type is " ++ ty | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty @@ -558,7 +558,7 @@ let rec explain_evar_kind env sigma evk ty = function assert false | Evar_kinds.VarInstance id -> strbrk "an instance of type " ++ ty ++ - str " for the variable " ++ pr_id id + str " for the variable " ++ Id.print id | Evar_kinds.SubEvar evk' -> let evi = Evd.find sigma evk' in let pc = match evi.evar_body with @@ -598,7 +598,7 @@ let explain_unsolvable_implicit env sigma evk explain = explain_placeholder_kind env sigma evi.evar_concl explain ++ pe let explain_var_not_found env id = - str "The variable" ++ spc () ++ pr_id id ++ + str "The variable" ++ spc () ++ Id.print id ++ spc () ++ str "was not found" ++ spc () ++ str "in the current" ++ spc () ++ str "environment" ++ str "." @@ -638,7 +638,7 @@ let explain_no_occurrence_found env sigma c id = str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++ str " in " ++ (match id with - | Some id -> pr_id id + | Some id -> Id.print id | None -> str"the current goal") ++ str "." let explain_cannot_unify_binding_type env sigma m n = @@ -660,7 +660,7 @@ let explain_wrong_abstraction_type env sigma na abs expected result = let abs = EConstr.to_constr sigma abs in let expected = EConstr.to_constr sigma expected in let result = EConstr.to_constr sigma result in - let ppname = match na with Name id -> pr_id id ++ spc () | _ -> mt () in + let ppname = match na with Name id -> Id.print id ++ spc () | _ -> mt () in str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ pr_lconstr_env env sigma expected ++ strbrk " with abstraction " ++ pr_lconstr_env env sigma abs ++ strbrk " of incompatible type " ++ @@ -723,9 +723,9 @@ let explain_type_error env sigma err = let pr_position (cl,pos) = let clpos = match cl with | None -> str " of the goal" - | Some (id,Locus.InHyp) -> str " of hypothesis " ++ pr_id id - | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ pr_id id - | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ pr_id id in + | Some (id,Locus.InHyp) -> str " of hypothesis " ++ Id.print id + | Some (id,Locus.InHypTypeOnly) -> str " of the type of hypothesis " ++ Id.print id + | Some (id,Locus.InHypValueOnly) -> str " of the body of hypothesis " ++ Id.print id in int pos ++ clpos let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1),t1) e = @@ -844,7 +844,7 @@ let explain_not_match_error = function | ModuleTypeFieldExpected -> strbrk "a module type is expected" | NotConvertibleInductiveField id | NotConvertibleConstructorField id -> - str "types given to " ++ pr_id id ++ str " differ" + str "types given to " ++ Id.print id ++ str " differ" | NotConvertibleBodyField -> str "the body of definitions differs" | NotConvertibleTypeField (env, typ1, typ2) -> @@ -869,7 +869,7 @@ let explain_not_match_error = function | RecordProjectionsExpected nal -> (if List.length nal >= 2 then str "expected projection names are " else str "expected projection name is ") ++ - pr_enum (function Name id -> pr_id id | _ -> str "_") nal + pr_enum (function Name id -> Id.print id | _ -> str "_") nal | NotEqualInductiveAliases -> str "Aliases to inductive types do not match" | NoTypeConstraintExpected -> @@ -1016,7 +1016,7 @@ let explain_not_a_class env c = pr_constr_env env Evd.empty c ++ str" is not a declared type class." let explain_unbound_method env cid id = - str "Unbound method name " ++ Nameops.pr_id (snd id) ++ spc () ++ + str "Unbound method name " ++ Id.print (snd id) ++ spc () ++ str"of class" ++ spc () ++ pr_global cid ++ str "." let pr_constr_exprs exprs = @@ -1061,7 +1061,7 @@ let explain_intro_needs_product () = let explain_does_not_occur_in c hyp = str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ - str "does not occur in" ++ spc () ++ pr_id hyp ++ str "." + str "does not occur in" ++ spc () ++ Id.print hyp ++ str "." let explain_non_linear_proof c = str "Cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++ @@ -1072,7 +1072,7 @@ let explain_meta_in_type c = str " of another meta" let explain_no_such_hyp id = - str "No such hypothesis: " ++ pr_id id + str "No such hypothesis: " ++ Id.print id let explain_refiner_error = function | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty @@ -1102,7 +1102,7 @@ let error_ill_formed_inductive env c v = let error_ill_formed_constructor env id c v nparams nargs = let pv = pr_lconstr_env env Evd.empty v in let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in - str "The type of constructor" ++ brk(1,1) ++ pr_id id ++ brk(1,1) ++ + str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++ str "is not valid;" ++ brk(1,1) ++ strbrk (if atomic then "it must be " else "its conclusion must be ") ++ pv ++ @@ -1130,17 +1130,17 @@ let error_bad_ind_parameters env c n v1 v2 = str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "." let error_same_names_types id = - str "The name" ++ spc () ++ pr_id id ++ spc () ++ + str "The name" ++ spc () ++ Id.print id ++ spc () ++ str "is used more than once." let error_same_names_constructors id = - str "The constructor name" ++ spc () ++ pr_id id ++ spc () ++ + str "The constructor name" ++ spc () ++ Id.print id ++ spc () ++ str "is used more than once." let error_same_names_overlap idl = strbrk "The following names are used both as type names and constructor " ++ str "names:" ++ spc () ++ - prlist_with_sep pr_comma pr_id idl ++ str "." + prlist_with_sep pr_comma Id.print idl ++ str "." let error_not_an_arity env c = str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++ diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index be9de5b30..7b8a38d5f 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -217,7 +217,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 (pr_id id ++ str " already exists."); + user_err ?loc (Id.print id ++ str " already exists."); id | None -> let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in @@ -294,7 +294,7 @@ let save_anonymous ?export_seff proof save_ident = let warn_let_as_axiom = CWarnings.create ~name:"let-as-axiom" ~category:"vernacular" - (fun id -> strbrk "Let definition" ++ spc () ++ pr_id id ++ + (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++ spc () ++ strbrk "declared as an axiom.") let admit (id,k,e) pl hook () = diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 9376afa8c..6c3dfec7d 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -310,7 +310,7 @@ let rec get_notation_vars onlyprint = function (* don't check for nonlinearity if printing only, see Bug 5526 *) if not onlyprint && Id.List.mem id vars then user_err ~hdr:"Metasyntax.get_notation_vars" - (str "Variable " ++ pr_id id ++ str " occurs more than once.") + (str "Variable " ++ Id.print id ++ str " occurs more than once.") else id::vars | (Terminal _ | Break _) :: sl -> get_notation_vars onlyprint sl | SProdList _ :: _ -> assert false @@ -323,7 +323,7 @@ let analyze_notation_tokens ~onlyprint l = let error_not_same_scope x y = user_err ~hdr:"Metasyntax.error_not_name_scope" - (str "Variables " ++ pr_id x ++ str " and " ++ pr_id y ++ str " must be in the same scope.") + (str "Variables " ++ Id.print x ++ str " and " ++ Id.print y ++ str " must be in the same scope.") (**********************************************************************) (* Build pretty-printing rules *) @@ -398,7 +398,7 @@ let check_open_binder isopen sl m = | _ -> assert false in if isopen && not (List.is_empty sl) then - user_err (str "as " ++ pr_id m ++ + user_err (str "as " ++ Id.print m ++ str " is a non-closed binder, no such \"" ++ prlist_with_sep spc pr_token sl ++ strbrk "\" is allowed to occur.") @@ -865,7 +865,7 @@ 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,_)::_ -> user_err ~hdr:"Metasyntax.check_useless_entry_types" - (pr_id x ++ str " is unbound in the notation.") + (Id.print x ++ str " is unbound in the notation.") | _ -> () let check_binder_type recvars etyps = @@ -922,7 +922,7 @@ let join_auxiliary_recursive_types recvars etyps = | Some xtyp, Some ytyp when Pervasives.(=) xtyp ytyp -> typs (* FIXME *) | Some xtyp, Some ytyp -> user_err - (strbrk "In " ++ pr_id x ++ str " .. " ++ pr_id y ++ + (strbrk "In " ++ Id.print x ++ str " .. " ++ Id.print y ++ strbrk ", both ends have incompatible types.")) recvars etyps diff --git a/vernac/obligations.ml b/vernac/obligations.ml index e23146273..364557bb4 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -437,7 +437,7 @@ let close sec = let keys = map_keys !from_prg in user_err ~hdr:"Program" (str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++ - prlist_with_sep spc (fun x -> Nameops.pr_id x) keys ++ + prlist_with_sep spc (fun x -> Id.print x) keys ++ (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++ str "unsolved obligations")) @@ -716,10 +716,10 @@ 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 + let progs = prlist_with_sep pr_comma Id.print progs in 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 "\"")) + ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\"")) let get_any_prog () = let prg_infos = !from_prg in diff --git a/vernac/record.ml b/vernac/record.ml index 1fd43624a..1bd47a556 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -138,7 +138,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs = let arity = EConstr.it_mkProd_or_LetIn typ newps in let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in let assums = List.filter is_local_assum newps in - let params = List.map (RelDecl.get_name %> out_name) assums in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in let ty = Inductive (params,(finite != BiFinite)) in let impls_env = compute_internalization_env env0 ~impls:impls_env ty [id] [EConstr.to_constr !evars arity] [imps] in let env2,impls,newfs,data = @@ -194,24 +194,24 @@ let warning_or_error coe indsp err = let st = match err with | MissingProj (fi,projs) -> let s,have = if List.length projs > 1 then "s","were" else "","was" in - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because the projection" ++ str s ++ spc () ++ - prlist_with_sep pr_comma pr_id projs ++ spc () ++ str have ++ + prlist_with_sep pr_comma Id.print projs ++ spc () ++ str have ++ strbrk " not defined.") | BadTypedProj (fi,ctx,te) -> match te with | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) -> - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because it is informative and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) -> - (pr_id fi ++ + (Id.print fi ++ strbrk" cannot be defined because it is large and " ++ Printer.pr_inductive (Global.env()) indsp ++ strbrk " is not.") | _ -> - (pr_id fi ++ strbrk " cannot be defined because it is not typable.") + (Id.print fi ++ strbrk " cannot be defined because it is not typable.") in if coe then user_err ~hdr:"structure" st; warn_cannot_define_projection (hov 0 st) @@ -240,7 +240,7 @@ let subst_projection fid l c = | Projection t -> lift depth t | NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k | NoProjection Anonymous -> - user_err (str "Field " ++ pr_id fid ++ + user_err (str "Field " ++ Id.print fid ++ str " depends on the " ++ pr_nth (k-depth-1) ++ str " field which has no name.") else diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7eedf24f8..5bcb3b1e1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -84,10 +84,10 @@ let show_intro all = let l,_= decompose_prod_assum sigma (Termops.strip_outer_cast sigma (pf_concl gl)) in if all then let lid = Tactics.find_intro_names l gl in - Feedback.msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) + Feedback.msg_notice (hov 0 (prlist_with_sep spc Id.print lid)) else if not (List.is_empty l) then let n = List.last l in - Feedback.msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + Feedback.msg_notice (Id.print (List.hd (Tactics.find_intro_names [n] gl))) end (** Prepare a "match" template for a given inductive type. @@ -252,7 +252,7 @@ let print_namespace ns = (* spiwack: I'm ignoring the dirpath, is that bad? *) let (mp,_,lbl) = Names.KerName.repr kn in let qn = (qualified_minus (List.length ns) mp)@[Names.Label.to_id lbl] in - print_list pr_id qn + print_list Id.print qn in let print_constant k body = (* FIXME: universes *) @@ -272,7 +272,7 @@ let print_namespace ns = acc ) constants (str"") in - Feedback.msg_notice ((print_list pr_id ns)++str":"++fnl()++constants_in_namespace) + Feedback.msg_notice ((print_list Id.print ns)++str":"++fnl()++constants_in_namespace) let print_strategy r = let open Conv_oracle in @@ -656,7 +656,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef ?loc mp "mod"; - Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is declared"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -678,7 +678,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info - (str "Interactive Module " ++ pr_id id ++ str " started"); + (str "Interactive Module " ++ Id.print id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -696,14 +696,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info - (str "Module " ++ pr_id id ++ str " is defined"); + (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; - Flags.if_verbose Feedback.msg_info (str "Module " ++ pr_id id ++ str " is defined"); + Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -725,7 +725,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info - (str "Interactive Module Type " ++ pr_id id ++ str " started"); + (str "Interactive Module Type " ++ Id.print id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -744,12 +744,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info - (str "Module Type " ++ pr_id id ++ str " is defined") + (str "Module Type " ++ Id.print id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; - Flags.if_verbose Feedback.msg_info (str "Module Type " ++ pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -874,7 +874,7 @@ let vernac_set_used_variables e = List.iter (fun id -> if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then user_err ~hdr:"vernac_set_used_variables" - (str "Unknown variable: " ++ pr_id id)) + (str "Unknown variable: " ++ Id.print id)) l; let _, to_clear = Proof_global.set_used_variables l in let to_clear = List.map snd to_clear in @@ -1628,7 +1628,7 @@ let print_about_hyp_globs ?loc ref_or_by_not glopt = let natureofid = match decl with | LocalAssum _ -> "Hypothesis" | LocalDef (_,bdy,_) ->"Constant (let in)" in - v 0 (pr_id id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() + v 0 (Id.print id ++ str":" ++ pr_econstr (NamedDecl.get_type decl) ++ fnl() ++ fnl() ++ str natureofid ++ str " of the goal context.") with (* fallback to globals *) | NoHyp | Not_found -> print_about ref_or_by_not @@ -1859,7 +1859,7 @@ let vernac_show = let open Feedback in function | ShowExistentials -> show_top_evars () | ShowUniverses -> show_universes () | ShowProofNames -> - msg_notice (pr_sequence pr_id (Proof_global.get_all_proof_names())) + msg_notice (pr_sequence Id.print (Proof_global.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id |