diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 6 | ||||
| -rw-r--r-- | vernac/command.ml | 6 | ||||
| -rw-r--r-- | vernac/himsg.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 12 |
4 files changed, 15 insertions, 15 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index cf534f13a..b99ccbf4a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -533,7 +533,7 @@ open Namegen let compute_bl_goal ind lnamesparrec nparrec = let eqI, eff = eqI ind lnamesparrec in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in @@ -676,7 +676,7 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let eqI, eff = eqI ind lnamesparrec in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and @@ -806,7 +806,7 @@ let compute_dec_goal ind lnamesparrec nparrec = check_not_is_defined (); let eq = Lazy.force eq and tt = Lazy.force tt and bb = Lazy.force bb in let list_id = list_id lnamesparrec in - let avoid = List.fold_right (Nameops.name_fold (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in + let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> id::l)) (List.map RelDecl.get_name lnamesparrec) [] in let create_input c = let x = next_ident_away (Id.of_string "x") avoid and y = next_ident_away (Id.of_string "y") avoid in diff --git a/vernac/command.ml b/vernac/command.ml index e2ebb4d7f..6ece585a9 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -411,8 +411,8 @@ let mk_mltype_data evdref env assums arity indname = (is_ml_type,indname,assums) let prepare_param = function - | LocalAssum (na,t) -> out_name na, LocalAssumEntry t - | LocalDef (na,b,_) -> out_name na, LocalDefEntry b + | LocalAssum (na,t) -> Name.get_id na, LocalAssumEntry t + | LocalDef (na,b,_) -> Name.get_id na, LocalDefEntry b (** Make the arity conclusion flexible to avoid generating an upper bound universe now, only if the universe does not appear anywhere else. @@ -590,7 +590,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite = (* Names of parameters as arguments of the inductive type (defs removed) *) let assums = List.filter is_local_assum ctx_params in - let params = List.map (RelDecl.get_name %> out_name) assums in + let params = List.map (RelDecl.get_name %> Name.get_id) assums in (* Interpret the arities *) let arities = List.map (interp_ind_arity env_params evdref) indl in diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 17bb87f2a..6d8dd82ac 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -682,12 +682,12 @@ let explain_wrong_abstraction_type env sigma na abs expected result = let explain_abstraction_over_meta _ m n = strbrk "Too complex unification problem: cannot find a solution for both " ++ - pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "." + Name.print m ++ spc () ++ str "and " ++ Name.print n ++ str "." let explain_non_linear_unification env sigma m t = let t = EConstr.to_constr sigma t in strbrk "Cannot unambiguously instantiate " ++ - pr_name m ++ str ":" ++ + Name.print m ++ str ":" ++ strbrk " which would require to abstract twice on " ++ pr_lconstr_env env sigma t ++ str "." @@ -1055,7 +1055,7 @@ let explain_refiner_bad_type arg ty conclty = let explain_refiner_unresolved_bindings l = str "Unable to find an instance for the " ++ str (String.plural (List.length l) "variable") ++ spc () ++ - prlist_with_sep pr_comma pr_name l ++ str"." + prlist_with_sep pr_comma Name.print l ++ str"." let explain_refiner_cannot_apply t harg = str "In refiner, a term of type" ++ brk(1,1) ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 6c1d64cfe..405d37927 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1003,12 +1003,12 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags let err_extra_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "Extra arguments: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let err_missing_args names = user_err ~hdr:"vernac_declare_arguments" (strbrk "The following arguments are not declared: " ++ - prlist_with_sep pr_comma pr_name names ++ str ".") + prlist_with_sep pr_comma Name.print names ++ str ".") in let rec check_extra_args extra_args = @@ -1093,14 +1093,14 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags match !example_renaming with | None -> mt () | Some (o,n) -> - str "Argument " ++ pr_name o ++ - str " renamed to " ++ pr_name n ++ str "."); + str "Argument " ++ Name.print o ++ + str " renamed to " ++ Name.print n ++ str "."); let duplicate_names = List.duplicates Name.equal (List.filter ((!=) Anonymous) names) in if not (List.is_empty duplicate_names) then begin - let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in + let duplicates = prlist_with_sep pr_comma Name.print duplicate_names in user_err (strbrk "Some argument names are duplicated: " ++ duplicates) end; @@ -1129,7 +1129,7 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags anonymous argument implicit *) | Anonymous :: _, (name, _) :: _ -> user_err ~hdr:"vernac_declare_arguments" - (strbrk"Argument "++ pr_name name ++ + (strbrk"Argument "++ Name.print name ++ strbrk " cannot be declared implicit.") | Name id :: inf_names, (name, impl) :: implicits -> |