diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 71ae8a1ec..25d0fcec9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -179,9 +179,9 @@ let make_cases s = | [] -> [] | (n,_)::l -> let n' = Namegen.next_name_away_in_cases_pattern n avoid in - string_of_id n' :: rename (n'::avoid) l in + Id.to_string n' :: rename (n'::avoid) l in let al' = rename [] al in - (string_of_id consname :: al') :: l) + (Id.to_string consname :: al') :: l) carr tarr [] | _ -> raise Not_found @@ -189,7 +189,7 @@ let make_cases s = let show_match id = let patterns = - try make_cases (string_of_id (snd id)) + try make_cases (Id.to_string (snd id)) with Not_found -> error "Unknown inductive type." in let pr_branch l = @@ -259,7 +259,7 @@ let print_namespace ns = begin match match_dirpath ns dir with | Some [] as y -> y | Some (a::ns') -> - if Int.equal (Names.id_ord a id) 0 then Some ns' + if Int.equal (Names.Id.compare a id) 0 then Some ns' else None | None -> None end @@ -272,7 +272,7 @@ let print_namespace ns = begin match match_modulepath ns mp with | Some [] as y -> y | Some (a::ns') -> - if Int.equal (Names.id_ord a id) 0 then Some ns' + if Int.equal (Names.Id.compare a id) 0 then Some ns' else None | None -> None end @@ -618,7 +618,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"; - if_verbose msg_info (str ("Module "^ string_of_id id ^" is declared")); + if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared")); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -639,7 +639,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Interactive Module "^ string_of_id id ^" started")); + (str ("Interactive Module "^ Id.to_string id ^" started")); List.iter (fun (export,id) -> Option.iter @@ -660,14 +660,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Module "^ string_of_id id ^" is defined")); + (str ("Module "^ Id.to_string id ^" is defined")); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref loc mp "mod"; - if_verbose msg_info (str ("Module "^ string_of_id id ^" is defined")); + if_verbose msg_info (str ("Module "^ Id.to_string id ^" 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 = @@ -687,7 +687,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = Modintern.interp_modtype id binders_ast mty_sign in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Interactive Module Type "^ string_of_id id ^" started")); + (str ("Interactive Module Type "^ Id.to_string id ^" started")); List.iter (fun (export,id) -> Option.iter @@ -707,12 +707,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = id binders_ast mty_sign mty_ast_l in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Module Type "^ string_of_id id ^" is defined")) + (str ("Module Type "^ Id.to_string id ^" is defined")) let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref loc mp "modtype"; - if_verbose msg_info (str ("Module Type "^ string_of_id id ^" is defined")) + if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined")) let vernac_include l = Declaremods.declare_include Modintern.interp_modexpr_or_modtype l @@ -824,8 +824,8 @@ let vernac_set_used_variables l = if not (List.distinct l) then error "Used variables list contains duplicates"; let vars = Environ.named_context (Global.env ()) in List.iter (fun id -> - if not (List.exists (fun (id',_,_) -> id_eq id id') vars) then - error ("Unknown variable: " ^ string_of_id id)) + if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then + error ("Unknown variable: " ^ Id.to_string id)) l; set_used_variables l @@ -914,7 +914,7 @@ let vernac_declare_arguments local r l nargs flags = let sr = smart_global r in let inf_names = Impargs.compute_implicits_names (Global.env()) (Global.type_of_global sr) in - let string_of_name = function Anonymous -> "_" | Name id -> string_of_id id in + let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in let rec check li ld ls = match li, ld, ls with | [], [], [] -> () | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls @@ -960,10 +960,10 @@ let vernac_declare_arguments local r l nargs flags = let sr', impl = List.fold_map (fun b -> function | (Anonymous, _,_, true, max), Name id -> assert false | (Name x, _,_, true, _), Anonymous -> - error ("Argument "^string_of_id x^" cannot be declared implicit.") + error ("Argument "^Id.to_string x^" cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> - b || not (id_eq iid id), Some (ExplByName id, max, false) - | (Name iid, _,_, _, _), Name id -> b || not (id_eq iid id), None + b || not (Id.equal iid id), Some (ExplByName id, max, false) + | (Name iid, _,_, _, _), Name id -> b || not (Id.equal iid id), None | _ -> b, None) sr (List.combine il inf_names) in sr || sr', List.map_filter (fun x -> x) impl) @@ -1412,7 +1412,7 @@ let interp_search_restriction = function open Search -let is_ident s = try ignore (check_ident s); true with UserError _ -> false +let is_ident s = try ignore (Id.check s); true with UserError _ -> false let interp_search_about_item = function | SearchSubPattern pat -> @@ -1537,7 +1537,7 @@ let vernac_abort = function | Some id -> Backtrack.mark_unreachable [snd id]; delete_proof id; - let s = string_of_id (snd id) in + let s = Id.to_string (snd id) in if_verbose msg_info (str ("Goal "^s^" aborted")) let vernac_abort_all () = |