aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/goal.ml14
-rw-r--r--proofs/goal.mli6
-rw-r--r--proofs/logic.ml74
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/pfedit.mli16
-rw-r--r--proofs/proof_global.ml26
-rw-r--r--proofs/proof_global.mli14
-rw-r--r--proofs/proof_type.ml22
-rw-r--r--proofs/proof_type.mli22
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/refiner.ml2
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli52
-rw-r--r--proofs/tactic_debug.ml4
-rw-r--r--proofs/tactic_debug.mli4
16 files changed, 133 insertions, 133 deletions
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6b672d2cb..38e536ba2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -279,16 +279,16 @@ let recheck_typability (what,id) env sigma t =
with _ ->
let s = match what with
| None -> "the conclusion"
- | Some id -> "hypothesis "^(Names.string_of_id id) in
+ | Some id -> "hypothesis "^(Names.Id.to_string id) in
Errors.error
- ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))
+ ("The correctness of "^s^" relies on the body of "^(Names.Id.to_string id))
let remove_hyp_body env sigma id =
let sign =
wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
(fun (_,c,t) _ ->
match c with
- | None -> Errors.error ((Names.string_of_id id)^" is not a local definition")
+ | None -> Errors.error ((Names.Id.to_string id)^" is not a local definition")
| Some c ->(id,None,t))
(fun (id',c,t as d) sign ->
(
@@ -384,9 +384,9 @@ let convert_hyp check (id,b,bt as d) env rdefs gl info =
let replace_function =
(fun _ (_,c,ct) _ ->
if check && not (Reductionops.is_conv env sigma bt ct) then
- Errors.error ("Incorrect change of the type of "^(Names.string_of_id id));
+ Errors.error ("Incorrect change of the type of "^(Names.Id.to_string id));
if check && not (Option.equal (Reductionops.is_conv env sigma) b c) then
- Errors.error ("Incorrect change of the body of "^(Names.string_of_id id));
+ Errors.error ("Incorrect change of the body of "^(Names.Id.to_string id));
d)
in
(* Modified named context. *)
@@ -427,9 +427,9 @@ let rename_hyp_sign id1 id2 sign =
(fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
let rename_hyp id1 id2 env rdefs gl info =
let hyps = hyps env rdefs gl info in
- if not (Names.id_eq id1 id2) &&
+ if not (Names.Id.equal id1 id2) &&
List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
- Errors.error ((Names.string_of_id id2)^" is already used.");
+ Errors.error ((Names.Id.to_string id2)^" is already used.");
let new_hyps = rename_hyp_sign id1 id2 hyps in
let new_env = Environ.reset_with_named_context new_hyps env in
let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 762bcf643..1146d95f6 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -102,10 +102,10 @@ val refine : refinable -> subgoals sensitive
(*** Cleaning goals ***)
(* Implements the [clear] tactic *)
-val clear : Names.identifier list -> subgoals sensitive
+val clear : Names.Id.t list -> subgoals sensitive
(* Implements the [clearbody] tactic *)
-val clear_body : Names.identifier list -> subgoals sensitive
+val clear_body : Names.Id.t list -> subgoals sensitive
(*** Conversion in goals ***)
@@ -121,7 +121,7 @@ val convert_concl : bool -> Term.constr -> subgoals sensitive
(*** Bureaucracy in hypotheses ***)
(* Renames a hypothesis. *)
-val rename_hyp : Names.identifier -> Names.identifier -> subgoals sensitive
+val rename_hyp : Names.Id.t -> Names.Id.t -> subgoals sensitive
(*** Sensitive primitives ***)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index b8341f1aa..ba85be766 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -34,7 +34,7 @@ type refiner_error =
(* Errors raised by the tactics *)
| IntroNeedsProduct
- | DoesNotOccurIn of constr * identifier
+ | DoesNotOccurIn of constr * Id.t
exception RefinerError of refiner_error
@@ -58,7 +58,7 @@ let rec catchable_exception = function
| _ -> false
let error_no_such_hypothesis id =
- error ("No such hypothesis: " ^ string_of_id id ^ ".")
+ error ("No such hypothesis: " ^ Id.to_string id ^ ".")
(* Tells if the refiner should check that the submitted rules do not
produce invalid subgoals *)
@@ -103,16 +103,16 @@ let recheck_typability (what,id) env sigma t =
with _ ->
let s = match what with
| None -> "the conclusion"
- | Some id -> "hypothesis "^(string_of_id id) in
+ | Some id -> "hypothesis "^(Id.to_string id) in
error
- ("The correctness of "^s^" relies on the body of "^(string_of_id id))
+ ("The correctness of "^s^" relies on the body of "^(Id.to_string id))
let remove_hyp_body env sigma id =
let sign =
apply_to_hyp_and_dependent_on (named_context_val env) id
(fun (_,c,t) _ ->
match c with
- | None -> error ((string_of_id id)^" is not a local definition.")
+ | None -> error ((Id.to_string id)^" is not a local definition.")
| Some c ->(id,None,t))
(fun (id',c,t as d) sign ->
(if !check then
@@ -134,36 +134,36 @@ let remove_hyp_body env sigma id =
(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
(* reculees par rapport aux autres (faire le contraire!) *)
-let mt_q = (Idmap.empty,[])
+let mt_q = (Id.Map.empty,[])
let push_val y = function
(_,[] as q) -> q
- | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
+ | (m, (x,l)::q) -> (m, (x,Id.Set.add y l)::q)
let push_item x v (m,l) =
- (Idmap.add x v m, (x,Idset.empty)::l)
-let mem_q x (m,_) = Idmap.mem x m
+ (Id.Map.add x v m, (x,Id.Set.empty)::l)
+let mem_q x (m,_) = Id.Map.mem x m
let find_q x (m,q) =
- let v = Idmap.find x m in
- let m' = Idmap.remove x m in
+ let v = Id.Map.find x m in
+ let m' = Id.Map.remove x m in
let rec find accs acc = function
[] -> raise Not_found
| [(x',l)] ->
- if id_eq x x' then ((v,Idset.union accs l),(m',List.rev acc))
+ if Id.equal x x' then ((v,Id.Set.union accs l),(m',List.rev acc))
else raise Not_found
| (x',l as i)::((x'',l'')::q as itl) ->
- if id_eq x x' then
- ((v,Idset.union accs l),
- (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
- else find (Idset.union l accs) (i::acc) itl in
- find Idset.empty [] q
+ if Id.equal x x' then
+ ((v,Id.Set.union accs l),
+ (m',List.rev acc@(x'',Id.Set.add x (Id.Set.union l l''))::q))
+ else find (Id.Set.union l accs) (i::acc) itl in
+ find Id.Set.empty [] q
let occur_vars_in_decl env hyps d =
- if Idset.is_empty hyps then false else
+ if Id.Set.is_empty hyps then false else
let ohyps = global_vars_set_of_decl env d in
- Idset.exists (fun h -> Idset.mem h ohyps) hyps
+ Id.Set.exists (fun h -> Id.Set.mem h ohyps) hyps
let reorder_context env sign ord =
- let ords = List.fold_right Idset.add ord Idset.empty in
- if not (Int.equal (List.length ord) (Idset.cardinal ords)) then
+ let ords = List.fold_right Id.Set.add ord Id.Set.empty in
+ if not (Int.equal (List.length ord) (Id.Set.cardinal ords)) then
error "Order list has duplicates";
let rec step ord expected ctxt_head moved_hyps ctxt_tail =
match ord with
@@ -175,15 +175,15 @@ let reorder_context env sign ord =
(str "Cannot move declaration " ++ pr_id top ++ spc() ++
str "before " ++
pr_sequence pr_id
- (Idset.elements (Idset.inter h
+ (Id.Set.elements (Id.Set.inter h
(global_vars_set_of_decl env d))));
step ord' expected ctxt_head mh (d::ctxt_tail)
| _ ->
(match ctxt_head with
| [] -> error_no_such_hypothesis (List.hd ord)
| (x,_,_ as d) :: ctxt ->
- if Idset.mem x expected then
- step ord (Idset.remove x expected)
+ if Id.Set.mem x expected then
+ step ord (Id.Set.remove x expected)
ctxt (push_item x d moved_hyps) ctxt_tail
else
step ord expected
@@ -200,7 +200,7 @@ let check_decl_position env sign (x,_,_ as d) =
let needed = global_vars_set_of_decl env d in
let deps = dependency_closure env (named_context_of_val sign) needed in
if List.mem x deps then
- error ("Cannot create self-referring hypothesis "^string_of_id x);
+ error ("Cannot create self-referring hypothesis "^Id.to_string x);
x::deps
(* Auxiliary functions for primitive MOVE tactic
@@ -212,8 +212,8 @@ let check_decl_position env sign (x,_,_ as d) =
* If [with_dep] then dependent hypotheses are moved accordingly. *)
let move_location_eq m1 m2 = match m1, m2 with
-| MoveAfter id1, MoveAfter id2 -> id_eq id1 id2
-| MoveBefore id1, MoveBefore id2 -> id_eq id1 id2
+| MoveAfter id1, MoveAfter id2 -> Id.equal id1 id2
+| MoveBefore id1, MoveBefore id2 -> Id.equal id1 id2
| MoveLast, MoveLast -> true
| MoveFirst, MoveFirst -> true
| _ -> false
@@ -221,7 +221,7 @@ let move_location_eq m1 m2 = match m1, m2 with
let rec get_hyp_after h = function
| [] -> error_no_such_hypothesis h
| (hyp,_,_) :: right ->
- if id_eq hyp h then
+ if Id.equal hyp h then
match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst
else
get_hyp_after h right
@@ -230,11 +230,11 @@ let split_sign hfrom hto l =
let rec splitrec left toleft = function
| [] -> error_no_such_hypothesis hfrom
| (hyp,c,typ) as d :: right ->
- if id_eq hyp hfrom then
+ if Id.equal hyp hfrom then
(left,right,d, toleft || move_location_eq hto MoveLast)
else
let is_toleft = match hto with
- | MoveAfter h' | MoveBefore h' -> id_eq hyp h'
+ | MoveAfter h' | MoveBefore h' -> Id.equal hyp h'
| _ -> false
in
splitrec (d::left) (toleft || is_toleft)
@@ -471,9 +471,9 @@ let convert_hyp sign sigma (id,b,bt as d) =
(fun _ (_,c,ct) _ ->
let env = Global.env_of_context sign in
if !check && not (is_conv env sigma bt ct) then
- error ("Incorrect change of the type of "^(string_of_id id)^".");
+ error ("Incorrect change of the type of "^(Id.to_string id)^".");
if !check && not (Option.equal (is_conv env sigma) b c) then
- error ("Incorrect change of the body of "^(string_of_id id)^".");
+ error ("Incorrect change of the body of "^(Id.to_string id)^".");
if !check then reorder := check_decl_position env sign d;
d) in
reorder_val_context env sign' !reorder
@@ -495,7 +495,7 @@ let prim_refiner r sigma goal =
(* Logical rules *)
| Intro id ->
if !check && mem_named_context id (named_context_of_val sign) then
- error ("Variable " ^ string_of_id id ^ " is already declared.");
+ error ("Variable " ^ Id.to_string id ^ " is already declared.");
(match kind_of_term (strip_outer_cast cl) with
| Prod (_,c1,b) ->
let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
@@ -524,7 +524,7 @@ let prim_refiner r sigma goal =
cl,sigma
else
(if !check && mem_named_context id (named_context_of_val sign) then
- error ("Variable " ^ string_of_id id ^ " is already declared.");
+ error ("Variable " ^ Id.to_string id ^ " is already declared.");
push_named_context_val (id,None,t) sign,cl,sigma) in
let (sg2,ev2,sigma) =
Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
@@ -556,7 +556,7 @@ let prim_refiner r sigma goal =
"mutual inductive declaration.");
if !check && mem_named_context f (named_context_of_val sign) then
error
- ("Name "^string_of_id f^" already used in the environment");
+ ("Name "^Id.to_string f^" already used in the environment");
mk_sign (push_named_context_val (f,None,ar) sign) oth
| [] ->
Goal.list_map (fun sigma (_,_,c) ->
@@ -679,9 +679,9 @@ let prim_refiner r sigma goal =
([gl], sigma)
| Rename (id1,id2) ->
- if !check && not (id_eq id1 id2) &&
+ if !check && not (Id.equal id1 id2) &&
List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
- error ((string_of_id id2)^" is already used.");
+ error ((Id.to_string id2)^" is already used.");
let sign' = rename_hyp id1 id2 sign in
let cl' = replace_vars [id1,mkVar id2] cl in
let (gl,ev,sigma) = mk_goal sign' cl' in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 75d9bd957..e87adb165 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -47,7 +47,7 @@ type refiner_error =
(*i Errors raised by the tactics i*)
| IntroNeedsProduct
- | DoesNotOccurIn of constr * identifier
+ | DoesNotOccurIn of constr * Id.t
exception RefinerError of refiner_error
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 44c5d7f30..ad334e91c 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -156,7 +156,7 @@ let build_constant_by_tactic id sign typ tac =
raise e
let build_by_tactic env typ tac =
- let id = id_of_string ("temporary_proof"^string_of_int (next())) in
+ let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = val_of_named_context (named_context env) in
(build_constant_by_tactic id sign typ tac).const_entry_body
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 382dd598d..1b2ae9ec7 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -38,7 +38,7 @@ val check_no_pending_proofs : unit -> unit
(** [delete_proof name] deletes proof of name [name] or fails if no proof
has this name *)
-val delete_proof : identifier located -> unit
+val delete_proof : Id.t located -> unit
(** [delete_current_proof ()] deletes current focused proof or fails if
no proof is focused *)
@@ -75,7 +75,7 @@ val current_proof_depth: unit -> int
type lemma_possible_guards = Proof_global.lemma_possible_guards
val start_proof :
- identifier -> goal_kind -> named_context_val -> constr ->
+ Id.t -> goal_kind -> named_context_val -> constr ->
?init_tac:tactic -> ?compute_guard:lemma_possible_guards ->
unit declaration_hook -> unit
@@ -91,7 +91,7 @@ val restart_proof : unit -> unit
it also tells if the guardness condition has to be inferred. *)
val cook_proof : (Proof.proof -> unit) ->
- identifier *
+ Id.t *
(Entries.definition_entry * lemma_possible_guards * goal_kind *
unit declaration_hook)
@@ -117,19 +117,19 @@ val get_current_goal_context : unit -> Evd.evar_map * env
(** [current_proof_statement] *)
val current_proof_statement :
- unit -> identifier * goal_kind * types * unit declaration_hook
+ unit -> Id.t * goal_kind * types * unit declaration_hook
(** {6 ... } *)
(** [get_current_proof_name ()] return the name of the current focused
proof or failed if no proof is focused *)
-val get_current_proof_name : unit -> identifier
+val get_current_proof_name : unit -> Id.t
(** [get_all_proof_names ()] returns the list of all pending proof names.
The first name is the current proof, the other names may come in
any order. *)
-val get_all_proof_names : unit -> identifier list
+val get_all_proof_names : unit -> Id.t list
(** {6 ... } *)
(** [set_end_tac tac] applies tactic [tac] to all subgoal generate
@@ -140,7 +140,7 @@ val set_end_tac : tactic -> unit
(** {6 ... } *)
(** [set_used_variables l] declares that section variables [l] will be
used in the proof *)
-val set_used_variables : identifier list -> unit
+val set_used_variables : Id.t list -> unit
val get_used_variables : unit -> Sign.section_context option
(** {6 ... } *)
@@ -165,7 +165,7 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
(** [build_by_tactic typ tac] returns a term of type [typ] by calling [tac] *)
-val build_constant_by_tactic : identifier -> named_context_val -> types -> tactic ->
+val build_constant_by_tactic : Id.t -> named_context_val -> types -> tactic ->
Entries.definition_entry
val build_by_tactic : env -> types -> tactic -> constr
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 9cc726beb..c5a190228 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -60,7 +60,7 @@ let _ =
(*** Proof Global Environment ***)
(* local shorthand *)
-type nproof = identifier*Proof.proof
+type nproof = Id.t*Proof.proof
(* Extra info on proofs. *)
type lemma_possible_guards = int list list
@@ -75,7 +75,7 @@ type proof_info = {
(* The head of [!current_proof] is the actual current proof, the other ones are
to be resumed when the current proof is closed or aborted. *)
let current_proof = ref ([]:nproof list)
-let proof_info = ref (Idmap.empty : proof_info Idmap.t)
+let proof_info = ref (Id.Map.empty : proof_info Id.Map.t)
(* Current proof_mode, for bookkeeping *)
let current_proof_mode = ref !default_proof_mode
@@ -84,7 +84,7 @@ let current_proof_mode = ref !default_proof_mode
let update_proof_mode () =
match !current_proof with
| (id,_)::_ ->
- let { mode = m } = Idmap.find id !proof_info in
+ let { mode = m } = Id.Map.find id !proof_info in
!current_proof_mode.reset ();
current_proof_mode := m;
!current_proof_mode.set ()
@@ -103,7 +103,7 @@ let _ = Errors.register_handler begin function
end
let extract id l =
let rec aux = function
- | ((id',_) as np)::l when id_eq id id' -> (np,l)
+ | ((id',_) as np)::l when Id.equal id id' -> (np,l)
| np::l -> let (np', l) = aux l in (np' , np::l)
| [] -> raise NoSuchProof
in
@@ -128,9 +128,9 @@ let find_top l =
(* combinators for the proof_info map *)
let add id info m =
- m := Idmap.add id info !m
+ m := Id.Map.add id info !m
let remove id m =
- m := Idmap.remove id !m
+ m := Id.Map.remove id !m
(*** Proof Global manipulation ***)
@@ -183,7 +183,7 @@ let discard_current () =
let discard_all () =
current_proof := [];
- proof_info := Idmap.empty
+ proof_info := Id.Map.empty
(* [set_proof_mode] sets the proof mode to be used after it's called. It is
typically called by the Proof Mode command. *)
@@ -191,9 +191,9 @@ let discard_all () =
No undo handling.
Applies to proof [id], and proof mode [m]. *)
let set_proof_mode m id =
- let info = Idmap.find id !proof_info in
+ let info = Id.Map.find id !proof_info in
let info = { info with mode = m } in
- proof_info := Idmap.add id info !proof_info;
+ proof_info := Id.Map.add id info !proof_info;
update_proof_mode ()
(* Complete function.
Handles undo.
@@ -223,7 +223,7 @@ end
let start_proof id str goals ?(compute_guard=[]) hook =
begin
List.iter begin fun (id_ex,_) ->
- if Names.id_eq id id_ex then raise AlreadyExists
+ if Names.Id.equal id id_ex then raise AlreadyExists
end !current_proof
end;
let p = Proof.start goals in
@@ -247,7 +247,7 @@ let set_endline_tactic tac =
let set_used_variables l =
let p = give_me_the_proof () in
let env = Global.env () in
- let ids = List.fold_right Idset.add l Idset.empty in
+ let ids = List.fold_right Id.Set.add l Id.Set.empty in
let ctx = Environ.keep_hyps env ids in
Proof.set_used_variables ctx p
@@ -274,7 +274,7 @@ let close_proof () =
proofs_and_types
in
let { compute_guard=cg ; strength=str ; hook=hook } =
- Idmap.find id !proof_info
+ Id.Map.find id !proof_info
in
(id, (entries,cg,str,hook))
with
@@ -405,7 +405,7 @@ module V82 = struct
let p = give_me_the_proof () in
let id = get_current_proof_name () in
let { strength=str ; hook=hook } =
- Idmap.find id !proof_info
+ Id.Map.find id !proof_info
in
(id,(Proof.V82.get_initial_conclusions p, str, hook))
end
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 3b43f61f9..33a0bf98a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -32,10 +32,10 @@ val there_is_a_proof : unit -> bool
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
-val get_current_proof_name : unit -> Names.identifier
-val get_all_proof_names : unit -> Names.identifier list
+val get_current_proof_name : unit -> Names.Id.t
+val get_all_proof_names : unit -> Names.Id.t list
-val discard : Names.identifier Loc.located -> unit
+val discard : Names.Id.t Loc.located -> unit
val discard_current : unit -> unit
val discard_all : unit -> unit
@@ -53,7 +53,7 @@ val give_me_the_proof : unit -> Proof.proof
proof end (e.g. to declare the built constructions as a coercion
or a setoid morphism). *)
type lemma_possible_guards = int list list
-val start_proof : Names.identifier ->
+val start_proof : Names.Id.t ->
Decl_kinds.goal_kind ->
(Environ.env * Term.types) list ->
?compute_guard:lemma_possible_guards ->
@@ -61,7 +61,7 @@ val start_proof : Names.identifier ->
unit
val close_proof : unit ->
- Names.identifier *
+ Names.Id.t *
(Entries.definition_entry list *
lemma_possible_guards *
Decl_kinds.goal_kind *
@@ -77,7 +77,7 @@ val run_tactic : unit Proofview.tactic -> unit
val set_endline_tactic : unit Proofview.tactic -> unit
(** Sets the section variables assumed by the proof *)
-val set_used_variables : Names.identifier list -> unit
+val set_used_variables : Names.Id.t list -> unit
val get_used_variables : unit -> Sign.section_context option
(** Appends the endline tactic of the current proof to a tactic. *)
@@ -127,5 +127,5 @@ module Bullet : sig
end
module V82 : sig
- val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
+ val get_current_initial_conclusions : unit -> Names.Id.t *(Term.types list * Decl_kinds.goal_kind * unit Tacexpr.declaration_hook)
end
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index b7237f1fc..eadf870fb 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -27,18 +27,18 @@ type goal = Goal.goal
type tactic = goal sigma -> goal list sigma
type prim_rule =
- | Intro of identifier
- | Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list * int
- | Cofix of identifier * (identifier * constr) list * int
+ | Intro of Id.t
+ | Cut of bool * bool * Id.t * types
+ | FixRule of Id.t * int * (Id.t * int * constr) list * int
+ | Cofix of Id.t * (Id.t * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
- | Thin of identifier list
- | ThinBody of identifier list
- | Move of bool * identifier * identifier move_location
- | Order of identifier list
- | Rename of identifier * identifier
+ | Thin of Id.t list
+ | ThinBody of Id.t list
+ | Move of bool * Id.t * Id.t move_location
+ | Order of Id.t list
+ | Rename of Id.t * Id.t
| Change_evars
(** Nowadays, the only rules we'll consider are the primitive rules *)
@@ -51,9 +51,9 @@ type ltac_call_kind =
| LtacNotationCall of string
| LtacNameCall of ltac_constant
| LtacAtomCall of glob_atomic_tactic_expr
- | LtacVarCall of identifier * glob_tactic_expr
+ | LtacVarCall of Id.t * glob_tactic_expr
| LtacConstrInterp of glob_constr *
- (extended_patvar_map * (identifier * identifier option) list)
+ (extended_patvar_map * (Id.t * Id.t option) list)
type ltac_trace = (int * Loc.t * ltac_call_kind) list
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 95ca33e90..37d5c4544 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -23,18 +23,18 @@ open Misctypes
is used by [Proof_tree] and [Refiner] *)
type prim_rule =
- | Intro of identifier
- | Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list * int
- | Cofix of identifier * (identifier * constr) list * int
+ | Intro of Id.t
+ | Cut of bool * bool * Id.t * types
+ | FixRule of Id.t * int * (Id.t * int * constr) list * int
+ | Cofix of Id.t * (Id.t * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
- | Thin of identifier list
- | ThinBody of identifier list
- | Move of bool * identifier * identifier move_location
- | Order of identifier list
- | Rename of identifier * identifier
+ | Thin of Id.t list
+ | ThinBody of Id.t list
+ | Move of bool * Id.t * Id.t move_location
+ | Order of Id.t list
+ | Rename of Id.t * Id.t
| Change_evars
(** Nowadays, the only rules we'll consider are the primitive rules *)
@@ -76,9 +76,9 @@ type ltac_call_kind =
| LtacNotationCall of string
| LtacNameCall of ltac_constant
| LtacAtomCall of glob_atomic_tactic_expr
- | LtacVarCall of identifier * glob_tactic_expr
+ | LtacVarCall of Id.t * glob_tactic_expr
| LtacConstrInterp of glob_constr *
- (extended_patvar_map * (identifier * identifier option) list)
+ (extended_patvar_map * (Id.t * Id.t option) list)
type ltac_trace = (int * Loc.t * ltac_call_kind) list
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index e4b8697d1..be0cba3a1 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -44,7 +44,7 @@ let set_strategy_one ref l =
| OpaqueDef _ ->
errorlabstrm "set_transparent_const"
(str "Cannot make" ++ spc () ++
- Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+ Nametab.pr_global_env Id.Set.empty (ConstRef sp) ++
spc () ++ str "transparent because it was declared opaque.");
| _ -> Csymtable.set_transparent_const sp)
| _ -> ()
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 704dd9887..c83d5ca7a 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -204,7 +204,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
List.fold_left
(fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
^ (List.fold_left
- (fun acc (nm,_,_) -> (Names.string_of_id nm) ^ " " ^ acc)
+ (fun acc (nm,_,_) -> (Names.Id.to_string nm) ^ " " ^ acc)
"" lh))
"" newhyps in
pp (str (emacs_str "<infoH>")
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 66a9a9962..2b5114174 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -53,7 +53,7 @@ let pf_get_hyp gls id =
try
Sign.lookup_named id (pf_hyps gls)
with Not_found ->
- error ("No such hypothesis: " ^ (string_of_id id))
+ error ("No such hypothesis: " ^ (Id.to_string id))
let pf_get_hyp_typ gls id =
let (_,_,ty)= (pf_get_hyp gls id) in
@@ -72,7 +72,7 @@ let pf_get_new_ids ids gls =
let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id
-let pf_parse_const gls = compose (pf_global gls) id_of_string
+let pf_parse_const gls = compose (pf_global gls) Id.of_string
let pf_reduction_of_red_expr gls re c =
(fst (reduction_of_red_expr re)) (pf_env gls) (project gls) c
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index da9aecde9..328a3d65b 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -39,22 +39,22 @@ val apply_sig_tac :
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
val pf_hyps : goal sigma -> named_context
-(*i val pf_untyped_hyps : goal sigma -> (identifier * constr) list i*)
-val pf_hyps_types : goal sigma -> (identifier * types) list
-val pf_nth_hyp_id : goal sigma -> int -> identifier
+(*i val pf_untyped_hyps : goal sigma -> (Id.t * constr) list i*)
+val pf_hyps_types : goal sigma -> (Id.t * types) list
+val pf_nth_hyp_id : goal sigma -> int -> Id.t
val pf_last_hyp : goal sigma -> named_declaration
-val pf_ids_of_hyps : goal sigma -> identifier list
-val pf_global : goal sigma -> identifier -> constr
+val pf_ids_of_hyps : goal sigma -> Id.t list
+val pf_global : goal sigma -> Id.t -> constr
val pf_parse_const : goal sigma -> string -> constr
val pf_type_of : goal sigma -> constr -> types
val pf_check_type : goal sigma -> constr -> types -> unit
val pf_hnf_type_of : goal sigma -> constr -> types
-val pf_get_hyp : goal sigma -> identifier -> named_declaration
-val pf_get_hyp_typ : goal sigma -> identifier -> types
+val pf_get_hyp : goal sigma -> Id.t -> named_declaration
+val pf_get_hyp_typ : goal sigma -> Id.t -> types
-val pf_get_new_id : identifier -> goal sigma -> identifier
-val pf_get_new_ids : identifier list -> goal sigma -> identifier list
+val pf_get_new_id : Id.t -> goal sigma -> Id.t
+val pf_get_new_ids : Id.t list -> goal sigma -> Id.t list
val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
@@ -87,34 +87,34 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
(** {6 The most primitive tactics. } *)
val refiner : rule -> tactic
-val introduction_no_check : identifier -> tactic
-val internal_cut_no_check : bool -> identifier -> types -> tactic
-val internal_cut_rev_no_check : bool -> identifier -> types -> tactic
+val introduction_no_check : Id.t -> tactic
+val internal_cut_no_check : bool -> Id.t -> types -> tactic
+val internal_cut_rev_no_check : bool -> Id.t -> types -> tactic
val refine_no_check : constr -> tactic
val convert_concl_no_check : types -> cast_kind -> tactic
val convert_hyp_no_check : named_declaration -> tactic
-val thin_no_check : identifier list -> tactic
-val thin_body_no_check : identifier list -> tactic
+val thin_no_check : Id.t list -> tactic
+val thin_body_no_check : Id.t list -> tactic
val move_hyp_no_check :
- bool -> identifier -> identifier move_location -> tactic
-val rename_hyp_no_check : (identifier*identifier) list -> tactic
-val order_hyps : identifier list -> tactic
+ bool -> Id.t -> Id.t move_location -> tactic
+val rename_hyp_no_check : (Id.t*Id.t) list -> tactic
+val order_hyps : Id.t list -> tactic
val mutual_fix :
- identifier -> int -> (identifier * int * constr) list -> int -> tactic
-val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic
+ Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
+val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> tactic
(** {6 The most primitive tactics with consistency and type checking } *)
-val introduction : identifier -> tactic
-val internal_cut : bool -> identifier -> types -> tactic
-val internal_cut_rev : bool -> identifier -> types -> tactic
+val introduction : Id.t -> tactic
+val internal_cut : bool -> Id.t -> types -> tactic
+val internal_cut_rev : bool -> Id.t -> types -> tactic
val refine : constr -> tactic
val convert_concl : types -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
-val thin : identifier list -> tactic
-val thin_body : identifier list -> tactic
-val move_hyp : bool -> identifier -> identifier move_location -> tactic
-val rename_hyp : (identifier*identifier) list -> tactic
+val thin : Id.t list -> tactic
+val thin_body : Id.t list -> tactic
+val move_hyp : bool -> Id.t -> Id.t move_location -> tactic
+val rename_hyp : (Id.t*Id.t) list -> tactic
(** {6 Tactics handling a list of goals. } *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6f93ab725..afbc8bbe4 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -169,13 +169,13 @@ let db_pattern_rule debug num r =
(* Prints the hypothesis pattern identifier if it exists *)
let hyp_bound = function
| Anonymous -> " (unbound)"
- | Name id -> " (bound to "^(Names.string_of_id id)^")"
+ | Name id -> " (bound to "^(Names.Id.to_string id)^")"
(* Prints a matched hypothesis *)
let db_matched_hyp debug env (id,_,c) ido =
if is_debug debug then
msg_tac_debug (str "Hypothesis " ++
- str ((Names.string_of_id id)^(hyp_bound ido)^
+ str ((Names.Id.to_string id)^(hyp_bound ido)^
" has been matched: ") ++ print_constr_env env c)
(* Prints the matched conclusion *)
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index e456ad90b..2ba1b315b 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -46,7 +46,7 @@ val db_pattern_rule :
(** Prints a matched hypothesis *)
val db_matched_hyp :
- debug_info -> env -> identifier * constr option * constr -> name -> unit
+ debug_info -> env -> Id.t * constr option * constr -> name -> unit
(** Prints the matched conclusion *)
val db_matched_concl : debug_info -> env -> constr -> unit
@@ -78,4 +78,4 @@ val db_logic_failure : debug_info -> exn -> unit
(** Prints a logic failure message for a rule *)
val db_breakpoint : debug_info ->
- identifier Loc.located message_token list -> unit
+ Id.t Loc.located message_token list -> unit
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 01:42:32 +0000