aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml2
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml20
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/declare.ml4
-rw-r--r--kernel/names.mli28
-rw-r--r--kernel/nativecode.ml12
-rw-r--r--kernel/nativeinstr.mli2
-rw-r--r--kernel/nativevalues.ml2
-rw-r--r--kernel/nativevalues.mli4
-rw-r--r--kernel/term_typing.ml14
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli4
-rw-r--r--library/global.ml4
-rw-r--r--library/global.mli2
-rw-r--r--library/globnames.ml2
-rw-r--r--library/lib.ml2
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/evarsolve.ml8
-rw-r--r--pretyping/nativenorm.ml8
-rw-r--r--pretyping/pretyping.ml2
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--proofs/tacmach.mli12
-rw-r--r--stm/stm.ml6
-rw-r--r--tactics/eauto.ml2
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tacticals.mli16
-rw-r--r--tactics/tactics.ml2
-rw-r--r--tactics/tactics.mli6
-rw-r--r--vernac/auto_ind_decl.ml2
-rw-r--r--vernac/lemmas.ml2
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 258385abc..b906c3b59 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1021,7 +1021,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
@@ -1574,19 +1574,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 14:40:17 +0000