From c71e69a9be2094061e041d60614b090c8381f0b7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:14:38 +0100 Subject: [api] Deprecate all legacy uses of Name.Id in core. This is a first step towards some of the solutions proposed in #6008. --- engine/evarutil.ml | 2 +- engine/evarutil.mli | 2 +- engine/evd.ml | 20 ++++++++++---------- interp/constrextern.ml | 2 +- interp/declare.ml | 4 ++-- kernel/names.mli | 28 ++++++++++++++-------------- kernel/nativecode.ml | 12 ++++++------ kernel/nativeinstr.mli | 2 +- kernel/nativevalues.ml | 2 +- kernel/nativevalues.mli | 4 ++-- kernel/term_typing.ml | 14 +++++++------- kernel/type_errors.ml | 2 +- kernel/type_errors.mli | 4 ++-- library/global.ml | 4 ++-- library/global.mli | 2 +- library/globnames.ml | 2 +- library/lib.ml | 2 +- pretyping/constr_matching.ml | 2 +- pretyping/evarsolve.ml | 8 ++++---- pretyping/nativenorm.ml | 8 ++++---- pretyping/pretyping.ml | 2 +- pretyping/tacred.ml | 2 +- proofs/tacmach.mli | 12 ++++++------ stm/stm.ml | 6 +++--- tactics/eauto.ml | 2 +- tactics/tacticals.ml | 2 +- tactics/tacticals.mli | 16 ++++++++-------- tactics/tactics.ml | 2 +- tactics/tactics.mli | 6 +++--- vernac/auto_ind_decl.ml | 2 +- vernac/lemmas.ml | 2 +- 31 files changed, 90 insertions(+), 90 deletions(-) diff --git a/engine/evarutil.ml b/engine/evarutil.ml index eabfb7b39..38efcca05 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -306,7 +306,7 @@ let push_rel_decl_to_named_context sigma decl (subst, vsubst, avoid, nc) = in let extract_if_neq id = function | Anonymous -> None - | Name id' when id_ord id id' = 0 -> None + | Name id' when Id.compare id id' = 0 -> None | Name id' -> Some id' in let na = RelDecl.get_name decl in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index ee0fae3d4..2f85bc733 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -223,7 +223,7 @@ val push_rel_decl_to_named_context : evar_map -> rel_declaration -> ext_named_context -> ext_named_context val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> - named_context_val * types * constr list * csubst * (identifier*constr) list + named_context_val * types * constr list * csubst * (Id.t*constr) list val generalize_evar_over_rels : evar_map -> existential -> types * constr list diff --git a/engine/evd.ml b/engine/evd.ml index a668826a7..86ab2263f 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -370,17 +370,17 @@ val key : Id.t -> t -> Evar.t end = struct -type t = Id.t EvMap.t * existential_key Idmap.t +type t = Id.t EvMap.t * existential_key Id.Map.t -let empty = (EvMap.empty, Idmap.empty) +let empty = (EvMap.empty, Id.Map.empty) let add_name_newly_undefined id evk evi (evtoid, idtoev as names) = match id with | None -> names | Some id -> - if Idmap.mem id idtoev then + if Id.Map.mem id idtoev then user_err (str "Already an existential evar of name " ++ pr_id id); - (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) = if EvMap.mem evk evtoid then @@ -392,15 +392,15 @@ let remove_name_defined evk (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in match id with | None -> names - | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev) + | Some id -> (EvMap.remove evk evtoid, Id.Map.remove id idtoev) let rename evk id (evtoid, idtoev) = let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in match id' with - | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev) + | None -> (EvMap.add evk id evtoid, Id.Map.add id evk idtoev) | Some id' -> - if Idmap.mem id idtoev then anomaly (str "Evar name already in use."); - (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev)) + if Id.Map.mem id idtoev then anomaly (str "Evar name already in use."); + (EvMap.update evk id evtoid (* overwrite old name *), Id.Map.add id evk (Id.Map.remove id' idtoev)) let reassign_name_defined evk evk' (evtoid, idtoev as names) = let id = try Some (EvMap.find evk evtoid) with Not_found -> None in @@ -408,13 +408,13 @@ let reassign_name_defined evk evk' (evtoid, idtoev as names) = | None -> names (** evk' must not be defined *) | Some id -> (EvMap.add evk' id (EvMap.remove evk evtoid), - Idmap.add id evk' (Idmap.remove id idtoev)) + Id.Map.add id evk' (Id.Map.remove id idtoev)) let ident evk (evtoid, _) = try Some (EvMap.find evk evtoid) with Not_found -> None let key id (_, idtoev) = - Idmap.find id idtoev + Id.Map.find id idtoev end diff --git a/interp/constrextern.ml b/interp/constrextern.ml index bb4227b4a..bd6aa0911 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1192,7 +1192,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with | PSort s -> GSort s let extern_constr_pattern env sigma pat = - extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat) + extern true (None,[]) Id.Set.empty (glob_of_pat Id.Set.empty env sigma pat) let extern_rel_context where env sigma sign = let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in diff --git a/interp/declare.ml b/interp/declare.ml index 7fcb38296..bd8f3db50 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -464,7 +464,7 @@ let cache_universes (p, l) = let glob = Global.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> - ((Idmap.add id (p, lev) idl, + ((Id.Map.add id (p, lev) idl, Univ.LMap.add lev id lid), Univ.ContextSet.add_universe lev ctx)) (glob, Univ.ContextSet.empty) l @@ -525,7 +525,7 @@ let do_constraint poly l = (str "Cannot declare constraints on anonymous universes") | GType (Some (loc, Name id)) -> let names, _ = Global.global_universe_names () in - try loc, Idmap.find id names + try loc, Id.Map.find id names with Not_found -> user_err ?loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id) in diff --git a/kernel/names.mli b/kernel/names.mli index d111dd3c0..d97fd2b3a 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -546,28 +546,28 @@ val eq_ind_chk : inductive -> inductive -> bool (** {5 Identifiers} *) type identifier = Id.t -(** @deprecated Alias for [Id.t] *) +[@@ocaml.deprecated "Alias for [Id.t]"] -val string_of_id : identifier -> string -(** @deprecated Same as [Id.to_string]. *) +val string_of_id : Id.t -> string +[@@ocaml.deprecated "Same as [Id.to_string]."] -val id_of_string : string -> identifier -(** @deprecated Same as [Id.of_string]. *) +val id_of_string : string -> Id.t +[@@ocaml.deprecated "Same as [Id.of_string]."] -val id_ord : identifier -> identifier -> int -(** @deprecated Same as [Id.compare]. *) +val id_ord : Id.t -> Id.t -> int +[@@ocaml.deprecated "Same as [Id.compare]."] -val id_eq : identifier -> identifier -> bool -(** @deprecated Same as [Id.equal]. *) +val id_eq : Id.t -> Id.t -> bool +[@@ocaml.deprecated "Same as [Id.equal]."] -module Idset : Set.S with type elt = identifier and type t = Id.Set.t -(** @deprecated Same as [Id.Set]. *) +module Idset : Set.S with type elt = Id.t and type t = Id.Set.t +[@@ocaml.deprecated "Same as [Id.Set]."] -module Idpred : Predicate.S with type elt = identifier and type t = Id.Pred.t -(** @deprecated Same as [Id.Pred]. *) +module Idpred : Predicate.S with type elt = Id.t and type t = Id.Pred.t +[@@ocaml.deprecated "Same as [Id.Pred]."] module Idmap : module type of Id.Map -(** @deprecated Same as [Id.Map]. *) +[@@ocaml.deprecated "Same as [Id.Map]."] (** {5 Directory paths} *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e08d913bc..6e9991ac5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -59,7 +59,7 @@ type gname = | Gnormtbl of label option * int | Ginternal of string | Grel of int - | Gnamed of identifier + | Gnamed of Id.t let eq_gname gn1 gn2 = match gn1, gn2 with @@ -266,7 +266,7 @@ type primitive = | Mk_fix of rec_pos * int | Mk_cofix of int | Mk_rel of int - | Mk_var of identifier + | Mk_var of Id.t | Mk_proj | Is_accu | Is_int @@ -625,7 +625,7 @@ let decompose_MLlam c = (*s Global declaration *) type global = -(* | Gtblname of gname * identifier array *) +(* | Gtblname of gname * Id.t array *) | Gtblnorm of gname * lname array * mllambda array | Gtblfixtype of gname * lname array * mllambda array | Glet of gname * mllambda @@ -732,7 +732,7 @@ type env = env_bound : int; (* length of env_rel *) (* free variables *) env_urel : (int * mllambda) list ref; (* list of unbound rel *) - env_named : (identifier * mllambda) list ref; + env_named : (Id.t * mllambda) list ref; env_univ : lname option} let empty_env univ () = @@ -1955,8 +1955,8 @@ let is_code_loaded ~interactive name = if is_loaded_native_file s then true else (name := NotLinked; false) -let param_name = Name (id_of_string "params") -let arg_name = Name (id_of_string "arg") +let param_name = Name (Id.of_string "params") +let arg_name = Name (Id.of_string "arg") let compile_mind prefix ~interactive mb mind stack = let u = Declareops.inductive_polymorphic_context mb in diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 2353470f0..73f18f7a7 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -21,7 +21,7 @@ type uint = and lambda = | Lrel of name * int - | Lvar of identifier + | Lvar of Id.t | Lmeta of metavariable * lambda (* type *) | Levar of existential * lambda (* type *) | Lprod of lambda * lambda diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 7463a30fe..1c9996d89 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -52,7 +52,7 @@ type atom = | Aconstant of pconstant | Aind of pinductive | Asort of sorts - | Avar of identifier + | Avar of Id.t | Acase of annot_sw * accumulator * t * (t -> t) | Afix of t array * t array * rec_pos * int (* types, bodies, rec_pos, pos *) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 49b1e122d..0e2db8486 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -44,7 +44,7 @@ type atom = | Aconstant of pconstant | Aind of pinductive | Asort of sorts - | Avar of identifier + | Avar of Id.t | Acase of annot_sw * accumulator * t * (t -> t) | Afix of t array * t array * rec_pos * int | Acofix of t array * t array * int * t @@ -62,7 +62,7 @@ val mk_rels_accu : int -> int -> t array val mk_constant_accu : constant -> Univ.Level.t array -> t val mk_ind_accu : inductive -> Univ.Level.t array -> t val mk_sort_accu : sorts -> Univ.Level.t array -> t -val mk_var_accu : identifier -> t +val mk_var_accu : Id.t -> t val mk_sw_accu : annot_sw -> accumulator -> t -> (t -> t) val mk_prod_accu : name -> t -> t -> t val mk_fix_accu : rec_pos -> int -> t array -> t array -> t diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f93b24b3e..e28c8e826 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -385,10 +385,10 @@ let build_constant_declaration kn env result = let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in let inferred_set, declared_set = mk_set inferred, mk_set declared in if not (Id.Set.subset inferred_set declared_set) then - let l = Id.Set.elements (Idset.diff inferred_set declared_set) in + let l = Id.Set.elements (Id.Set.diff inferred_set declared_set) in let n = List.length l in - let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in - let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in + let declared_vars = Pp.pr_sequence Id.print (Id.Set.elements declared_set) in + let inferred_vars = Pp.pr_sequence Id.print (Id.Set.elements inferred_set) in let missing_vars = Pp.pr_sequence Id.print (List.rev l) in user_err Pp.(prlist str ["The following section "; (String.plural n "variable"); " "; @@ -414,7 +414,7 @@ let build_constant_declaration kn env result = we must look at the body NOW, if any *) let ids_typ = global_vars_set env typ in let ids_def = match def with - | Undef _ -> Idset.empty + | Undef _ -> Id.Set.empty | Def cs -> global_vars_set env (Mod_subst.force_constr cs) | OpaqueDef lc -> let vars = @@ -425,7 +425,7 @@ let build_constant_declaration kn env result = if !Flags.record_aux_file then record_aux env ids_typ vars; vars in - keep_hyps env (Idset.union ids_typ ids_def), def + keep_hyps env (Id.Set.union ids_typ ids_def), def | None -> if !Flags.record_aux_file then record_aux env Id.Set.empty Id.Set.empty; @@ -438,14 +438,14 @@ let build_constant_declaration kn env result = | Def cs as x -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env (Mod_subst.force_constr cs) in - let inferred = keep_hyps env (Idset.union ids_typ ids_def) in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in check declared inferred; x | OpaqueDef lc -> (* In this case we can postpone the check *) OpaqueDef (Opaqueproof.iter_direct_opaque (fun c -> let ids_typ = global_vars_set env typ in let ids_def = global_vars_set env c in - let inferred = keep_hyps env (Idset.union ids_typ ids_def) in + let inferred = keep_hyps env (Id.Set.union ids_typ ids_def) in check declared inferred) lc) in let univs = result.cook_universes in let tps = diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index bbaf569d3..9813fc566 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -44,7 +44,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of identifier * 'constr + | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 1b2ccf8f8..95a963da2 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -45,7 +45,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of identifier * 'constr + | ReferenceVariables of Id.t * 'constr | ElimArity of pinductive * sorts_family list * 'constr * ('constr, 'types) punsafe_judgment * (sorts_family * sorts_family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -74,7 +74,7 @@ val error_not_type : env -> unsafe_judgment -> 'a val error_assumption : env -> unsafe_judgment -> 'a -val error_reference_variables : env -> identifier -> constr -> 'a +val error_reference_variables : env -> Id.t -> constr -> 'a val error_elim_arity : env -> pinductive -> sorts_family list -> constr -> unsafe_judgment -> diff --git a/library/global.ml b/library/global.ml index 963c97741..28b9e66f8 100644 --- a/library/global.ml +++ b/library/global.ml @@ -233,11 +233,11 @@ let universes_of_global gr = (** Global universe names *) type universe_names = - (polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t + (polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t let global_universes = Summary.ref ~name:"Global universe names" - ((Idmap.empty, Univ.LMap.empty) : universe_names) + ((Id.Map.empty, Univ.LMap.empty) : universe_names) let global_universe_names () = !global_universes let set_global_universe_names s = global_universes := s diff --git a/library/global.mli b/library/global.mli index c777691d1..15bf58f82 100644 --- a/library/global.mli +++ b/library/global.mli @@ -104,7 +104,7 @@ val body_of_constant_body : Declarations.constant_body -> (Term.constr * Univ.AU (** Global universe name <-> level mapping *) type universe_names = - (Decl_kinds.polymorphic * Univ.universe_level) Idmap.t * Id.t Univ.LMap.t + (Decl_kinds.polymorphic * Univ.universe_level) Id.Map.t * Id.t Univ.LMap.t val global_universe_names : unit -> universe_names val set_global_universe_names : universe_names -> unit diff --git a/library/globnames.ml b/library/globnames.ml index dc9541a0d..5c75994dd 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -84,7 +84,7 @@ let is_global c t = | ConstRef c, Const (c', _) -> eq_constant c c' | IndRef i, Ind (i', _) -> eq_ind i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' - | VarRef id, Var id' -> id_eq id id' + | VarRef id, Var id' -> Id.equal id id' | _ -> false let printable_constr_of_global = function diff --git a/library/lib.ml b/library/lib.ml index 5418003eb..e95bb47f2 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -505,7 +505,7 @@ let variable_section_segment_of_reference = function let section_instance = function | VarRef id -> let eq = function - | Variable (id',_,_,_) -> Names.id_eq id id' + | Variable (id',_,_,_) -> Names.Id.equal id id' | Context _ -> false in if List.exists eq (pi1 (List.hd !sectab)) diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 9128d4042..ddef1cee9 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -213,7 +213,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels let open EConstr in let convref ref c = match ref, EConstr.kind sigma c with - | VarRef id, Var id' -> Names.id_eq id id' + | VarRef id, Var id' -> Names.Id.equal id id' | ConstRef c, Const (c',_) -> Names.eq_constant c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 7f81d1aa3..e88d8f89d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1011,7 +1011,7 @@ let closure_of_filter evd evk = function | Some filter -> let evi = Evd.find_undefined evd evk in let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in - let test b decl = b || Idset.mem (get_id decl) vars || + let test b decl = b || Id.Set.mem (get_id decl) vars || match decl with | LocalAssum _ -> false @@ -1561,19 +1561,19 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs = let rhs = whd_beta evd rhs (* heuristic *) in let fast rhs = let filter_ctxt = evar_filtered_context evi in - let names = ref Idset.empty in + let names = ref Id.Set.empty in let rec is_id_subst ctxt s = match ctxt, s with | (decl :: ctxt'), (c :: s') -> let id = get_id decl in - names := Idset.add id !names; + names := Id.Set.add id !names; isVarId evd id c && is_id_subst ctxt' s' | [], [] -> true | _ -> false in is_id_subst filter_ctxt (Array.to_list argsv) && closed0 evd rhs && - Idset.subset (collect_vars evd rhs) !names + Id.Set.subset (collect_vars evd rhs) !names in let body = if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *) diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 1038945c1..fe134f512 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -88,7 +88,7 @@ let invert_tag cst tag reloc_tbl = let decompose_prod env t = let (name,dom,codom as res) = destProd (whd_all env t) in match name with - | Anonymous -> (Name (id_of_string "x"),dom,codom) + | Anonymous -> (Name (Id.of_string "x"),dom,codom) | _ -> res let app_type env c = @@ -321,7 +321,7 @@ and nf_atom_type env sigma atom = mkCase(ci, p, a, branchs), tcase | Afix(tt,ft,rp,s) -> let tt = Array.map (fun t -> nf_type env sigma t) tt in - let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in + let name = Array.map (fun _ -> (Name (Id.of_string "Ffix"))) tt in let lvl = nb_rel env in let nbfix = Array.length ft in let fargs = mk_rels_accu lvl (Array.length ft) in @@ -334,7 +334,7 @@ and nf_atom_type env sigma atom = mkFix((rp,s),(name,tt,ft)), tt.(s) | Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) -> let tt = Array.map (nf_type env sigma) tt in - let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in + let name = Array.map (fun _ -> (Name (Id.of_string "Fcofix"))) tt in let lvl = nb_rel env in let fargs = mk_rels_accu lvl (Array.length ft) in let env = push_rec_types (name,tt,[||]) env in @@ -376,7 +376,7 @@ and nf_predicate env sigma ind mip params v pT = | Vfun f, _ -> let k = nb_rel env in let vb = f (mk_rel_accu k) in - let name = Name (id_of_string "c") in + let name = Name (Id.of_string "c") in let n = mip.mind_nrealargs in let rargs = Array.init n (fun i -> mkRel (n-i)) in let params = if Int.equal n 0 then params else Array.map (lift n) params in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 30783bfad..a69caecab 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -202,7 +202,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) = with Not_found -> try let id = try Id.of_string s with _ -> raise Not_found in - evd, snd (Idmap.find id names) + evd, snd (Id.Map.find id names) with Not_found -> if not (is_strict_universe_declarations ()) then new_univ_level_variable ?loc ~name:s univ_rigid evd diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 708788ab8..9451b0f86 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1051,7 +1051,7 @@ let contextually byhead occs f env sigma t = let match_constr_evaluable_ref sigma c evref = match EConstr.kind sigma c, evref with | Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u - | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty + | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty | _, _ -> None let substlin env sigma evalref n (nowhere_except_in,locs) c = diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d4e9555f3..de9f8e700 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -97,7 +97,7 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : identifier -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a @@ -118,13 +118,13 @@ module New : sig val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : identifier -> 'a Proofview.Goal.t -> identifier - val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list + val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t - val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list + val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list - val pf_get_hyp : identifier -> 'a Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> 'a Proofview.Goal.t -> types + val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types diff --git a/stm/stm.ml b/stm/stm.ml index 3cac3b609..6c22d3771 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -517,8 +517,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (let rec aux x = match x with - | VernacDefinition (_,((_,i),_),_) -> Names.string_of_id i - | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.string_of_id i + | VernacDefinition (_,((_,i),_),_) -> Names.Id.to_string i + | VernacStartTheoremProof (_,[Some ((_,i),_),_]) -> Names.Id.to_string i | VernacTime (_, e) | VernacTimeout (_, e) -> aux e | _ -> "branch" in aux x) @@ -3097,7 +3097,7 @@ let current_proof_depth ~doc = let unmangle n = let n = VCS.Branch.to_string n in let idx = String.index n '_' + 1 in - Names.id_of_string (String.sub n idx (String.length n - idx)) + Names.Id.of_string (String.sub n idx (String.length n - idx)) let proofname b = match VCS.get_branch b with | { VCS.kind = (`Proof _| `Edit _) } -> Some b diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2b5bbfcd1..9097aebd0 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -439,7 +439,7 @@ let autounfolds db occs cls gl = in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in - let ids = Idset.filter (fun id -> List.mem id hyps) ids in + let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in Proofview.V82.of_tactic (unfold_option unfolds cls) gl diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bce0dda10..07eea7b63 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -623,7 +623,7 @@ module New = struct let name_elim = match EConstr.kind sigma elim with | Const (kn, _) -> string_of_con kn - | Var id -> string_of_id id + | Var id -> Id.to_string id | _ -> "\b" in user_err ~hdr:"Tacticals.general_elim_then_using" diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2a04c413b..3abd42d46 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -226,12 +226,12 @@ module New : sig val nLastDecls : 'a Proofview.Goal.t -> int -> named_context - val ifOnHyp : (identifier * types -> bool) -> - (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> - identifier -> unit Proofview.tactic + val ifOnHyp : (Id.t * types -> bool) -> + (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> + Id.t -> unit Proofview.tactic - val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic - val onLastHypId : (identifier -> unit tactic) -> unit tactic + val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic + val onLastHypId : (Id.t -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic @@ -239,9 +239,9 @@ module New : sig (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic - val tryAllHyps : (identifier -> unit tactic) -> unit tactic - val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic - val onClause : (identifier option -> unit tactic) -> clause -> unit tactic + val tryAllHyps : (Id.t -> unit tactic) -> unit tactic + val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic + val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f8f9e029b..6f67606d2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1376,7 +1376,7 @@ let enforce_prop_bound_names rename tac = (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> string_of_id id + | Some id when not very_standard -> Id.to_string id | _ -> "" in Name (add_suffix Namegen.default_prop_ident s) else diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 32923ea81..98cf1b437 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -271,7 +271,7 @@ type eliminator = { val general_elim : evars_flag -> clear_flag -> constr with_bindings -> eliminator -> unit Proofview.tactic -val general_elim_clause : evars_flag -> unify_flags -> identifier option -> +val general_elim_clause : evars_flag -> unify_flags -> Id.t option -> clausenv -> eliminator -> unit Proofview.tactic val default_elim : evars_flag -> clear_flag -> constr with_bindings -> @@ -355,7 +355,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic val assert_after : Name.t -> types -> unit Proofview.tactic val assert_as : (* true = before *) bool -> - (* optionally tell if a specialization of some hyp: *) identifier option -> + (* optionally tell if a specialization of some hyp: *) Id.t option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactics assert, enough and pose proof; note that "by" @@ -428,7 +428,7 @@ module Simple : sig val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic val case : constr -> unit Proofview.tactic - val apply_in : identifier -> constr -> unit Proofview.tactic + val apply_in : Id.t -> constr -> unit Proofview.tactic end diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 7af391758..66a4a2e49 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -190,7 +190,7 @@ let build_beq_scheme mode kn = match EConstr.kind sigma c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants | Var x -> - let eid = id_of_string ("eq_"^(string_of_id x)) in + let eid = Id.of_string ("eq_"^(Id.to_string x)) in let () = try ignore (Environ.lookup_named eid env) with Not_found -> raise (ParameterWithoutEquality (VarRef x)) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 9ab89c883..dbf7fec66 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -506,7 +506,7 @@ let save_proof ?proof = function let env = Global.env () in let ids_typ = Environ.global_vars_set env typ in let ids_def = Environ.global_vars_set env pproof in - Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) + Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def)) | _ -> None in let decl = Proof_global.get_universe_decl () in let evd = Evd.from_ctx universes in -- cgit v1.2.3