Modulification of identifier

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7

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