From c571cdbbcac5cb4b4a5a19ab2f7ac51222316292 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Nov 2017 18:43:02 +0100 Subject: [api] Another large deprecation, `Nameops` --- vernac/himsg.ml | 50 +++++++++++++++++++++++++------------------------- 1 file changed, 25 insertions(+), 25 deletions(-) (limited to 'vernac/himsg.ml') 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 () ++ -- cgit v1.2.3