Modulification of identifier

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

15 files changed, 275 insertions, 282 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index c129306d2..ca73799c1 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -105,17 +105,17 @@ let make_refl_eq constructor type_of_t t  =
 
 type pte_info =
     {
-      proving_tac : (identifier list ->  Tacmach.tactic);
+      proving_tac : (Id.t list ->  Tacmach.tactic);
       is_valid : constr -> bool
     }
 
-type ptes_info = pte_info Idmap.t
+type ptes_info = pte_info Id.Map.t
 
 type 'a dynamic_info =
     {
       nb_rec_hyps : int;
-      rec_hyps : identifier list ;
-      eq_hyps : identifier list;
+      rec_hyps : Id.t list ;
+      eq_hyps : Id.t list;
       info : 'a
     }
 
@@ -361,7 +361,7 @@ let is_property (ptes_info:ptes_info) t_x full_type_of_hyp =
     if isVar pte && Array.for_all closed0 args
     then
       try
-	let info = Idmap.find (destVar pte) ptes_info in
+	let info = Id.Map.find (destVar pte) ptes_info in
 	info.is_valid full_type_of_hyp
       with Not_found -> false
     else false
@@ -406,7 +406,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
   do_rewrite eq_ids
 
 
-let rec_pte_id = id_of_string "Hrec"
+let rec_pte_id = Id.of_string "Hrec"
 let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
   let coq_False = Coqlib.build_coq_False () in
   let coq_True = Coqlib.build_coq_True () in
@@ -430,7 +430,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 	if is_property ptes_infos t_x actual_real_type_of_hyp then
 	  begin
 	    let pte,pte_args =  (destApp t_x) in
-	    let (* fix_info *) prove_rec_hyp = (Idmap.find (destVar pte) ptes_infos).proving_tac in
+	    let (* fix_info *) prove_rec_hyp = (Id.Map.find (destVar pte) ptes_infos).proving_tac in
 	    let popped_t' = Termops.pop t' in
 	    let real_type_of_hyp = it_mkProd_or_LetIn popped_t' context in
 	    let prove_new_type_of_hyp =
@@ -579,7 +579,7 @@ let clean_goal_with_heq ptes_infos continue_tac (dyn_infos:body_info) =
       ]
       g
 
-let heq_id = id_of_string "Heq"
+let heq_id = Id.of_string "Heq"
 
 let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
   fun g ->
@@ -632,7 +632,7 @@ let my_orelse tac1 tac2 g =
 (*     observe (str "using snd tac since : " ++ Errors.print e); *)
     tac2 g
 
-let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id =
+let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
   let args = Array.of_list (List.map mkVar  args_id) in
   let instanciate_one_hyp hid =
     my_orelse
@@ -672,10 +672,10 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	tclMAP instanciate_one_hyp hyps;
 	(fun g ->
 	   let all_g_hyps_id =
-	     List.fold_right Idset.add (pf_ids_of_hyps g) Idset.empty
+	     List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
 	   in
 	   let remaining_hyps =
-	     List.filter (fun id -> Idset.mem id all_g_hyps_id) hyps
+	     List.filter (fun id -> Id.Set.mem id all_g_hyps_id) hyps
 	   in
 	   do_prove remaining_hyps g
 	  )
@@ -885,7 +885,7 @@ let build_proof
 type static_fix_info =
     {
       idx : int;
-      name : identifier;
+      name : Id.t;
       types : types;
       offset : int;
       nb_realargs : int;
@@ -1042,7 +1042,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
       (fun na ->
 	 let new_id =
 	   match na with
-	       Name id -> fresh_id !avoid (string_of_id id)
+	       Name id -> fresh_id !avoid (Id.to_string id)
 	     | Anonymous -> fresh_id !avoid "H"
 	 in
 	 avoid := new_id :: !avoid;
@@ -1183,14 +1183,14 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		   in
 (* 		   observe (str "binding " ++ Ppconstr.pr_id (Nameops.out_name pte) ++  *)
 (* 			      str " to " ++ Ppconstr.pr_id info.name); *)
-		   (Idmap.add (Nameops.out_name pte) info acc_map,info::acc_info)
+		   (Id.Map.add (Nameops.out_name pte) info acc_map,info::acc_info)
 		   )
 		0
-		(Idmap.empty,[])
+		(Id.Map.empty,[])
 		(List.rev princ_info.predicates)
 	    in
 	    pte_to_fix,List.rev rev_info
-	| _ -> Idmap.empty,[]
+	| _ -> Id.Map.empty,[]
     in
     let mk_fixes : tactic =
       let pre_info,infos = list_chop fun_num infos in
@@ -1224,7 +1224,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 	let pte,pte_args = (decompose_app pte_app) in
 	try
 	  let pte = try destVar pte with _ -> anomaly "Property is not a variable"  in
-	  let fix_info = Idmap.find  pte ptes_to_fix in
+	  let fix_info = Id.Map.find  pte ptes_to_fix in
 	  let nb_args = fix_info.nb_realargs in
 	  tclTHENSEQ
 	    [
@@ -1262,7 +1262,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		       build_proof
 			 interactive_proof
 			 (Array.to_list fnames)
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 		     in
 		     let prove_tac branches  =
 		       let dyn_infos =
@@ -1272,7 +1272,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			 }
 		       in
 		       observe_tac "cleaning" (clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 			 do_prove
 			 dyn_infos)
 		     in
@@ -1316,7 +1316,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 		      build_proof
 			interactive_proof
 			(Array.to_list fnames)
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 		    in
 		    let prove_tac branches  =
 		      let dyn_infos =
@@ -1326,7 +1326,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
 			 }
 		      in
 		       clean_goal_with_heq
-			 (Idmap.map prove_rec_hyp ptes_to_fix)
+			 (Id.Map.map prove_rec_hyp ptes_to_fix)
 			 do_prove
 			 dyn_infos
 		    in
@@ -1413,7 +1413,7 @@ let rec rewrite_eqs_in_eqs eqs =
 	    (tclMAP
 	       (fun id gl ->
 		  observe_tac
-		    (Format.sprintf "rewrite %s in %s " (string_of_id eq) (string_of_id id))
+		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
 		    (tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences
 			       true (* dep proofs also: *) true id (mkVar eq) false))
 		    gl
@@ -1427,7 +1427,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
     (tclTHENSEQ
        [
 	 backtrack_eqs_until_hrec hrec eqs;
-	 (* observe_tac ("new_prove_with_tcc ( applying "^(string_of_id hrec)^" )" ) *)
+	 (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *)
 	 (tclTHENS  (* We must have exactly ONE subgoal !*)
 	    (apply (mkVar hrec))
 	    [ tclTHENSEQ
@@ -1463,13 +1463,13 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 
 
 let is_valid_hypothesis predicates_name =
-  let predicates_name = List.fold_right Idset.add predicates_name Idset.empty in
+  let predicates_name = List.fold_right Id.Set.add predicates_name Id.Set.empty in
   let is_pte typ =
     if isApp typ
     then
       let pte,_ = destApp typ in
       if isVar pte
-      then Idset.mem (destVar pte) predicates_name
+      then Id.Set.mem (destVar pte) predicates_name
       else false
     else false
   in
@@ -1491,7 +1491,7 @@ let prove_principle_for_gen
     fun na ->
       let new_id =
 	  match na with
-	    | Name id -> fresh_id !avoid (string_of_id id)
+	    | Name id -> fresh_id !avoid (Id.to_string id)
 	    | Anonymous -> fresh_id !avoid "H"
       in
       avoid := new_id :: !avoid;
@@ -1534,9 +1534,9 @@ let prove_principle_for_gen
   let subst_constrs = List.map (fun (na,_,_) -> mkVar (Nameops.out_name na)) (pre_rec_arg@princ_info.params) in
   let relation = substl subst_constrs relation in
   let input_type = substl subst_constrs rec_arg_type in
-  let wf_thm_id = Nameops.out_name (fresh_id (Name (id_of_string "wf_R"))) in
+  let wf_thm_id = Nameops.out_name (fresh_id (Name (Id.of_string "wf_R"))) in
   let acc_rec_arg_id =
-    Nameops.out_name (fresh_id (Name (id_of_string ("Acc_"^(string_of_id rec_arg_id)))))
+    Nameops.out_name (fresh_id (Name (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))))
   in
   let revert l =
     tclTHEN (h_generalize (List.map mkVar l)) (clear l)
@@ -1580,7 +1580,7 @@ let prove_principle_for_gen
     let hyps = pf_ids_of_hyps gls in
       let hid =
 	next_ident_away_in_goal
-	  (id_of_string "prov")
+	  (Id.of_string "prov")
 	  hyps
       in
       tclTHENSEQ
@@ -1669,14 +1669,14 @@ let prove_principle_for_gen
 	     is_valid = is_valid_hypothesis predicates_names
 	   }
 	 in
-	 let ptes_info : pte_info Idmap.t =
+	 let ptes_info : pte_info Id.Map.t =
 	   List.fold_left
 	     (fun map pte_id ->
-		Idmap.add pte_id
+		Id.Map.add pte_id
 		  pte_info
 		  map
 	     )
-	     Idmap.empty
+	     Id.Map.empty
 	     predicates_names
 	 in
 	 let make_proof rec_hyps =
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 533fbfaaa..1d30ce9a6 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -41,7 +41,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env = Global.env () in
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:identifier list) (predicates:rel_context)  : rel_context =
+  let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context)  : rel_context =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
@@ -83,10 +83,10 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   in
   let ptes_vars = List.map (fun (id,_,_) -> id) new_predicates in
   let is_pte =
-    let set = List.fold_right Idset.add ptes_vars Idset.empty in
+    let set = List.fold_right Id.Set.add ptes_vars Id.Set.empty in
     fun t ->
       match kind_of_term t with
-	| Var id -> Idset.mem id set
+	| Var id -> Id.Set.mem id set
 	| _ -> false
   in
   let pre_princ =
@@ -114,7 +114,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
       | Construct((_,num),_) -> num
       | _ -> assert false
   in
-  let dummy_var = mkVar (id_of_string "________") in
+  let dummy_var = mkVar (Id.of_string "________") in
   let mk_replacement c i args =
     let res = mkApp(rel_to_fun.(i), Array.map Termops.pop (array_get_start args)) in
 (*     observe (str "replacing " ++ pr_lconstr c ++ str " by "  ++ pr_lconstr res); *)
@@ -284,7 +284,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
   (*    Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
      observe (str "new_principle_type : " ++ pr_lconstr new_principle_type);
   let new_princ_name =
-    next_ident_away_in_goal (id_of_string "___________princ_________") []
+    next_ident_away_in_goal (Id.of_string "___________princ_________") []
   in
   begin
     Lemmas.start_proof
@@ -366,7 +366,7 @@ let generate_functional_principle
       begin
 	try
 	  let id = Pfedit.get_current_proof_name () in
-	  let s = string_of_id id in
+	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.sub s 0 n = "___________princ_________"
@@ -519,7 +519,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
       begin
 	try
 	  let id = Pfedit.get_current_proof_name () in
-	  let s = string_of_id id in
+	  let s = Id.to_string id in
 	  let n = String.length "___________princ_________" in
 	  if String.length s >= n
 	  then if String.sub s 0 n = "___________princ_________"
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 00d130d28..a16b834f8 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -10,7 +10,7 @@ val generate_functional_principle :
   (* *)
   sorts array option ->
   (* Name of the new principle *)
-  (identifier) option ->
+  (Id.t) option ->
   (* the compute functions to use   *)
   constant array ->
   (* We prove the nth- principle *)
@@ -29,6 +29,6 @@ exception No_graph_found
 
 val make_scheme : (constant*glob_sort) list -> Entries.definition_entry list
 
-val build_scheme : (identifier*Libnames.reference*glob_sort) list ->  unit
-val build_case_scheme : (identifier*Libnames.reference*glob_sort)  ->  unit
+val build_scheme : (Id.t*Libnames.reference*glob_sort) list ->  unit
+val build_case_scheme : (Id.t*Libnames.reference*glob_sort)  ->  unit
 
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 2fdf62d26..ef2276134 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -368,7 +368,7 @@ let find_fapp (test:constr -> bool) g : fapp_info list =
     an occurence of function [id] in the conclusion of goal [g]. If
     [id]=[None] then calls to any function are selected. In any case
     [heuristic] is used to select the most pertinent occurrence. *)
-let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info list)
+let finduction (oid:Id.t option) (heuristic: fapp_info list -> fapp_info list)
     (nexttac:Proof_type.tactic) g =
   let test = match oid with
     | Some id ->
@@ -468,10 +468,10 @@ VERNAC COMMAND EXTEND MergeFunind
        let ar2 = List.length (fst (decompose_prod f2type)) in
        let _ =
 	 if ar1 <> List.length cl1 then
-	   Errors.error ("not the right number of arguments for " ^ string_of_id id1) in
+	   Errors.error ("not the right number of arguments for " ^ Id.to_string id1) in
        let _ =
 	 if ar2 <> List.length cl2 then
-	   Errors.error ("not the right number of arguments for " ^ string_of_id id2) in
+	   Errors.error ("not the right number of arguments for " ^ Id.to_string id2) in
        Merge.merge id1 id2 (Array.of_list cl1) (Array.of_list cl2)  id
      ]
 END
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 593e274fb..cf7d8e8fe 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -57,7 +57,7 @@ type 'a build_entry_pre_return =
 type 'a build_entry_return =
     {
       result : 'a build_entry_pre_return list;
-      to_avoid : identifier list
+      to_avoid : Id.t list
     }
 
 (*
@@ -114,9 +114,9 @@ let ids_of_binder =  function
 let rec change_vars_in_binder mapping = function
     [] -> []
   | (bt,t)::l ->
-      let new_mapping = List.fold_right Idmap.remove (ids_of_binder bt) mapping in
+      let new_mapping = List.fold_right Id.Map.remove (ids_of_binder bt) mapping in
       (bt,change_vars mapping t)::
-	(if idmap_is_empty new_mapping
+	(if Id.Map.is_empty new_mapping
 	 then l
 	 else change_vars_in_binder new_mapping l
 	)
@@ -138,23 +138,23 @@ let apply_args ctxt body args =
   let need_convert avoid  bt =
     List.exists (need_convert_id avoid) (ids_of_binder bt)
   in
-  let next_name_away (na:name) (mapping: identifier Idmap.t) (avoid: identifier list) =
+  let next_name_away (na:name) (mapping: Id.t Id.Map.t) (avoid: Id.t list) =
     match na with
        | Name id when List.mem id avoid ->
 	   let new_id = Namegen.next_ident_away id avoid in
-	   Name new_id,Idmap.add id new_id mapping,new_id::avoid
+	   Name new_id,Id.Map.add id new_id mapping,new_id::avoid
        | _ -> na,mapping,avoid
   in
-  let next_bt_away bt (avoid:identifier list) =
+  let next_bt_away bt (avoid:Id.t list) =
     match bt with
       | LetIn na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  LetIn new_na,mapping,new_avoid
       | Prod na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Prod new_na,mapping,new_avoid
       | Lambda na ->
-	  let new_na,mapping,new_avoid = next_name_away na Idmap.empty avoid  in
+	  let new_na,mapping,new_avoid = next_name_away na Id.Map.empty avoid  in
 	  Lambda new_na,mapping,new_avoid
   in
   let rec do_apply avoid ctxt body args =
@@ -173,7 +173,7 @@ let apply_args ctxt body args =
 	      let new_avoid =  id::avoid in
 	      let new_id = Namegen.next_ident_away id new_avoid in
 	      let new_avoid' = new_id :: new_avoid in
-	      let mapping = Idmap.add id new_id Idmap.empty in
+	      let mapping = Id.Map.add id new_id Id.Map.empty in
 	      let new_ctxt' = change_vars_in_binder mapping ctxt' in
 	      let new_body = change_vars mapping body in
 	      new_avoid',new_ctxt',new_body,new_id
@@ -477,7 +477,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 			      GApp(Loc.ghost,t,l)
 		in
 		build_entry_lc env funnames avoid (aux f args)
-	    | GVar(_,id) when Idset.mem id funnames ->
+	    | GVar(_,id) when Id.Set.mem id funnames ->
 		(* if we have [f t1 ... tn] with [f]$\in$[fnames]
 		   then we create a fresh variable [res],
 		   add [res] and its "value" (i.e. [res v1 ... vn]) to each
@@ -725,7 +725,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	   (will be used in the following recursive calls)
 	*)
 	let new_env = List.fold_right2 add_pat_variables patl types env in
-	let not_those_patterns : (identifier list -> glob_constr -> glob_constr) list =
+	let not_those_patterns : (Id.t list -> glob_constr -> glob_constr) list =
 	  List.map2
 	    (fun pat typ ->
 	       fun avoid pat'_as_term ->
@@ -787,7 +787,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
-		      if Idset.mem id this_pat_ids
+		      if Id.Set.mem id this_pat_ids
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
@@ -835,7 +835,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 
 let is_res id =
   try
-    String.sub (string_of_id id) 0 4 = "_res"
+    String.sub (Id.to_string id) 0 4 = "_res"
   with Invalid_argument _ -> false
 
 
@@ -901,7 +901,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    (depth + 1) b
 			in
 			mkGProd(n,new_t,new_b),
-			Idset.filter not_free_in_t id_to_exclude
+			Id.Set.filter not_free_in_t id_to_exclude
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
@@ -1019,7 +1019,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		  (* J.F:. keep this comment  it explain how to remove some meaningless equalities
 		     if keep_eq then
 		     mkGProd(n,t,new_b),id_to_exclude
-		     else new_b, Idset.add id id_to_exclude
+		     else new_b, Id.Set.add id id_to_exclude
 		  *)
 	    | GApp(loc1,GRef(loc2,eq_as_ref),[ty;rt1;rt2])
 		when  eq_as_ref = Lazy.force Coqlib.coq_eq_ref  && n = Anonymous
@@ -1051,10 +1051,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	      end
 	    | _ ->
 		observe (str "computing new type for prod : " ++ pr_glob_constr rt);
@@ -1067,10 +1067,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (depth + 1) b
 		in
 		match n with
-		  | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
-		      new_b,Idset.remove id
-			(Idset.filter not_free_in_t id_to_exclude)
-		  | _ -> mkGProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args ->
+		      new_b,Id.Set.remove id
+			(Id.Set.filter not_free_in_t id_to_exclude)
+		  | _ -> mkGProd(n,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLambda(_,n,k,t,b) ->
 	begin
@@ -1087,11 +1087,11 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    (args@[mkGVar id])new_crossed_types
 		    (depth + 1 ) b
 		in
-		if Idset.mem id id_to_exclude && depth >= nb_args
+		if Id.Set.mem id id_to_exclude && depth >= nb_args
 		then
-		  new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  GProd(Loc.ghost,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude
+		  GProd(Loc.ghost,n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly "Should not have an anonymous function here"
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
@@ -1108,10 +1108,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      args (t::crossed_types)
 	      (depth + 1 ) b in
 	  match n with
-	    | Name id when Idset.mem id id_to_exclude && depth >= nb_args  ->
-		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude)
+	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
+		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 	    | _ -> GLetIn(Loc.ghost,n,t,new_b),
-		Idset.filter not_free_in_t id_to_exclude
+		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(_,nal,(na,rto),t,b) ->
 	assert (rto=None);
@@ -1133,15 +1133,15 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	      (depth + 1) b
 	  in
 (* 	  match n with  *)
-(* 	    | Name id when Idset.mem id id_to_exclude ->  *)
-(* 		new_b,Idset.remove id (Idset.filter not_free_in_t id_to_exclude) *)
+(* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
+(* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
 	  GLetTuple(Loc.ghost,nal,(na,None),t,new_b),
-		Idset.filter not_free_in_t (Idset.union id_to_exclude id_to_exclude')
+		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
 
-    | _ -> mkGApp(mkGVar  relname,args@[rt]),Idset.empty
+    | _ -> mkGApp(mkGVar  relname,args@[rt]),Id.Set.empty
 
 
 (* debuging wrapper *)
@@ -1164,7 +1164,7 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 *)
 let rec compute_cst_params relnames params = function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp(_,GVar(_,relname'),rtl) when Idset.mem relname' relnames ->
+  | GApp(_,GVar(_,relname'),rtl) when Id.Set.mem relname' relnames ->
       compute_cst_params_from_app [] (params,rtl)
   | GApp(_,f,args) ->
       List.fold_left (compute_cst_params relnames) params (f::args)
@@ -1182,7 +1182,7 @@ and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
     | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl'
-	when id_ord id id' == 0 && not is_defined ->
+	when Id.compare id id' == 0 && not is_defined ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
@@ -1233,7 +1233,7 @@ let do_build_inductive
     (rtl:glob_constr list) =
   let _time1 = System.get_time () in
 (*   Pp.msgnl (prlist_with_sep fnl Printer.pr_glob_constr rtl); *)
-  let funnames_as_set = List.fold_right Idset.add funnames Idset.empty in
+  let funnames_as_set = List.fold_right Id.Set.add funnames Id.Set.empty in
   let funnames = Array.of_list funnames in
   let funsargs = Array.of_list funsargs in
   let returned_types = Array.of_list returned_types in
@@ -1244,7 +1244,7 @@ let do_build_inductive
     Ensures by: obvious
     i*)
   let relnames = Array.map mk_rel_id funnames in
-  let relnames_as_set = Array.fold_right Idset.add relnames Idset.empty in
+  let relnames_as_set = Array.fold_right Id.Set.add relnames Id.Set.empty in
   (* Construction of the pseudo constructors *)
   let env =
     Array.fold_right
@@ -1264,12 +1264,12 @@ let do_build_inductive
 	(fun (n,t,is_defined) acc ->
 	   if is_defined
 	   then
-	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
+	     Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
 			      acc)
 	   else
 	     Constrexpr.CProdN
 	       (Loc.ghost,
-		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+		[[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
 		acc
 	       )
 	)
@@ -1307,9 +1307,9 @@ let do_build_inductive
     (*i The next call to mk_rel_id is valid since we are constructing the graph
       Ensures by: obvious
       i*)
-    id_of_string ((string_of_id (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
+    Id.of_string ((Id.to_string (mk_rel_id funnames.(i)))^"_"^(string_of_int !next_constructor_id))
   in
-  let rel_constructors i rt : (identifier*glob_constr) list =
+  let rel_constructors i rt : (Id.t*glob_constr) list =
     next_constructor_id := (-1);
     List.map (fun constr -> (mk_constructor_id i),constr) (constr i rt)
   in
@@ -1330,12 +1330,12 @@ let do_build_inductive
       (fun (n,t,is_defined) acc ->
 	 if is_defined
 	 then
-	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Idset.empty t,
+	   Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),Constrextern.extern_glob_constr Id.Set.empty t,
 			    acc)
 	 else
 	   Constrexpr.CProdN
 	   (Loc.ghost,
-	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Idset.empty t],
+	   [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,Constrextern.extern_glob_constr Id.Set.empty t],
 	    acc
 	   )
       )
@@ -1352,10 +1352,10 @@ let do_build_inductive
       (fun (n,t,is_defined) ->
 	 if is_defined
 	 then
-	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Idset.empty t)
+	   Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t)
 	 else
 	 Constrexpr.LocalRawAssum
-	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Idset.empty t)
+	   ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t)
       )
       rels_params
   in
@@ -1365,7 +1365,7 @@ let do_build_inductive
 	 false,((Loc.ghost,id),
 		Flags.with_option
 		  Flags.raw_print
-		  (Constrextern.extern_glob_type Idset.empty) ((* zeta_normalize *) t)
+		  (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) t)
 	       )
       ))
       (rel_constructors)
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index b8e7b3ab4..87fcb1022 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -8,7 +8,7 @@
 *)
 
 val build_inductive :
-  Names.identifier list -> (* The list of function name *)
+  Names.Id.t list -> (* The list of function name *)
   (Names.name*Glob_term.glob_constr*bool) list list -> (* The list of function args *)
   Constrexpr.constr_expr list -> (* The list of function returned type *)
   Glob_term.glob_constr list -> (* the list of body *)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index f678b898b..7785cbe59 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -6,9 +6,6 @@ open Names
 open Decl_kinds
 open Misctypes
 
-(* Ocaml 3.06 Map.S does not handle is_empty *)
-let idmap_is_empty m = m = Idmap.empty
-
 (*
    Some basic functions to rebuild glob_constr
    In each of them the location is Loc.ghost
@@ -119,7 +116,7 @@ let rec glob_make_or_list = function
 let remove_name_from_mapping mapping na =
   match na with
     | Anonymous -> mapping
-    | Name id -> Idmap.remove id mapping
+    | Name id -> Id.Map.remove id mapping
 
 let change_vars =
   let rec change_vars mapping rt =
@@ -128,7 +125,7 @@ let change_vars =
       | GVar(loc,id) ->
 	  let new_id =
 	    try
-	      Idmap.find id mapping
+	      Id.Map.find id mapping
 	    with Not_found -> id
 	  in
 	  GVar(loc,new_id)
@@ -187,8 +184,8 @@ let change_vars =
 	  GCast(loc,change_vars mapping b,
 		Miscops.map_cast_type (change_vars mapping) c)
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
-    let new_mapping = List.fold_right Idmap.remove idl mapping in
-    if idmap_is_empty new_mapping
+    let new_mapping = List.fold_right Id.Map.remove idl mapping in
+    if Id.Map.is_empty new_mapping
     then br
     else (loc,idl,patl,change_vars new_mapping res)
   in
@@ -200,27 +197,27 @@ let rec alpha_pat excluded pat =
   match pat with
     | PatVar(loc,Anonymous) ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	PatVar(loc,Name new_id),(new_id::excluded),Idmap.empty
+	PatVar(loc,Name new_id),(new_id::excluded),Id.Map.empty
     | PatVar(loc,Name id) ->
 	if List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
 	  PatVar(loc,Name new_id),(new_id::excluded),
-	(Idmap.add id new_id Idmap.empty)
-	else pat,excluded,Idmap.empty
+	(Id.Map.add id new_id Id.Map.empty)
+	else pat,excluded,Id.Map.empty
     | PatCstr(loc,constr,patl,na) ->
 	let new_na,new_excluded,map =
 	  match na with
 	    | Name id when List.mem id excluded ->
 		let new_id = Namegen.next_ident_away id excluded in
-		Name new_id,new_id::excluded, Idmap.add id new_id Idmap.empty
-	    | _ -> na,excluded,Idmap.empty
+		Name new_id,new_id::excluded, Id.Map.add id new_id Id.Map.empty
+	    | _ -> na,excluded,Id.Map.empty
 	in
 	let new_patl,new_excluded,new_map =
 	  List.fold_left
 	    (fun (patl,excluded,map) pat ->
 	       let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	       (new_pat::patl,new_excluded,Idmap.fold Idmap.add new_map map)
+	       (new_pat::patl,new_excluded,Id.Map.fold Id.Map.add new_map map)
 	    )
 	    ([],new_excluded,map)
 	    patl
@@ -232,9 +229,9 @@ let alpha_patl excluded patl  =
     List.fold_left
       (fun (patl,excluded,map) pat ->
 	 let new_pat,new_excluded,new_map = alpha_pat excluded pat in
-	 new_pat::patl,new_excluded,(Idmap.fold Idmap.add new_map map)
+	 new_pat::patl,new_excluded,(Id.Map.fold Id.Map.add new_map map)
       )
-      ([],excluded,Idmap.empty)
+      ([],excluded,Id.Map.empty)
       patl
   in
   (List.rev patl,new_excluded,map)
@@ -266,7 +263,7 @@ let rec alpha_rt excluded rt =
     match rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ -> rt
       | GLambda(loc,Anonymous,k,t,b) ->
-	  let new_id = Namegen.next_ident_away (id_of_string "_x") excluded in
+	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
 	  let new_excluded = new_id :: excluded in
 	  let new_t = alpha_rt new_excluded t in
 	  let new_b = alpha_rt new_excluded b in
@@ -285,7 +282,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_excluded = new_id::excluded in
@@ -299,7 +296,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_t = alpha_rt new_excluded t in
@@ -311,7 +308,7 @@ let rec alpha_rt excluded rt =
 	  if new_id = id
 	  then t,b
 	  else
-	    let replace = change_vars (Idmap.add id new_id Idmap.empty) in
+	    let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in
 	    (t,replace b)
 	in
 	let new_excluded = new_id::excluded in
@@ -332,14 +329,14 @@ let rec alpha_rt excluded rt =
 		     then
 		       na::nal,id::excluded,mapping
 		     else
-		       (Name new_id)::nal,id::excluded,(Idmap.add id new_id mapping)
+		       (Name new_id)::nal,id::excluded,(Id.Map.add id new_id mapping)
 	    )
-	    ([],excluded,Idmap.empty)
+	    ([],excluded,Id.Map.empty)
 	    nal
 	in
 	let new_nal = List.rev rev_new_nal in
 	let new_rto,new_t,new_b =
-	  if idmap_is_empty mapping
+	  if Id.Map.is_empty mapping
 	  then rto,t,b
 	  else let replace = change_vars mapping in
 	  (Option.map replace rto, t,replace b)
@@ -387,14 +384,14 @@ and alpha_br excluded (loc,ids,patl,res) =
 let is_free_in id =
   let rec is_free_in = function
     | GRef _ ->  false
-    | GVar(_,id') -> id_ord id' id == 0
+    | GVar(_,id') -> Id.compare id' id == 0
     | GEvar _ -> false
     | GPatVar _ -> false
     | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl)
     | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) ->
 	let check_in_b =
 	  match n with
-	    | Name id' -> id_ord id' id <> 0
+	    | Name id' -> Id.compare id' id <> 0
 	    | _ -> true
 	in
 	is_free_in t || (check_in_b && is_free_in b)
@@ -451,7 +448,7 @@ let replace_var_by_term x_id term =
   let rec replace_var_by_pattern rt =
     match rt with
       | GRef _ -> rt
-      | GVar(_,id) when id_ord id x_id == 0 -> term
+      | GVar(_,id) when Id.compare id x_id == 0 -> term
       | GVar _ -> rt
       | GEvar _ -> rt
       | GPatVar _ -> rt
@@ -460,7 +457,7 @@ let replace_var_by_term x_id term =
 	       replace_var_by_pattern rt',
 	       List.map replace_var_by_pattern rtl
 	      )
-      | GLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GLambda(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
       | GLambda(loc,name,k,t,b) ->
 	  GLambda(loc,
 		  name,
@@ -468,7 +465,7 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt
+      | GProd(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt
       | GProd(loc,name,k,t,b) ->
 	  GProd(loc,
 		  name,
@@ -476,7 +473,7 @@ let replace_var_by_term x_id term =
 		  replace_var_by_pattern t,
 		  replace_var_by_pattern b
 		 )
-      | GLetIn(_,Name id,_,_) when id_ord id x_id == 0 -> rt
+      | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt
       | GLetIn(loc,name,def,b) ->
 	  GLetIn(loc,
 		 name,
@@ -512,7 +509,7 @@ let replace_var_by_term x_id term =
 	  GCast(loc,replace_var_by_pattern b,
 		Miscops.map_cast_type replace_var_by_pattern c)
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
-    if List.exists (fun id -> id_ord id x_id == 0) idl
+    if List.exists (fun id -> Id.compare id x_id == 0) idl
     then br
     else (loc,idl,patl,replace_var_by_pattern res)
   in
@@ -573,13 +570,13 @@ let eq_cases_pattern pat1 pat2 =
 let ids_of_pat =
   let rec ids_of_pat ids = function
     | PatVar(_,Anonymous) -> ids
-    | PatVar(_,Name id) -> Idset.add id ids
+    | PatVar(_,Name id) -> Id.Set.add id ids
     | PatCstr(_,_,patl,_) -> List.fold_left ids_of_pat ids patl
   in
-  ids_of_pat Idset.empty
+  ids_of_pat Id.Set.empty
 
 let id_of_name = function
-  | Names.Anonymous -> id_of_string "x"
+  | Names.Anonymous -> Id.of_string "x"
   | Names.Name x -> x
 
 (* TODO: finish Rec caes *)
@@ -604,7 +601,7 @@ let ids_of_glob_constr c =
       | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
-  List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
+  List.fold_left (fun acc x -> Id.Set.add x acc) Id.Set.empty (ids_of_glob_constr [] c)
 
 
 
@@ -678,7 +675,7 @@ let expand_as =
     match pat with
       | PatVar _ -> map
       | PatCstr(_,_,patl,Name id) ->
-	  Idmap.add id (pattern_to_term pat) (List.fold_left add_as map patl)
+	  Id.Map.add id (pattern_to_term pat) (List.fold_left add_as map patl)
       | PatCstr(_,_,patl,_) -> List.fold_left add_as map patl
   in
   let rec expand_as map rt =
@@ -687,7 +684,7 @@ let expand_as =
       | GVar(_,id) ->
 	  begin
 	    try
-	      Idmap.find id map
+	      Id.Map.find id map
 	    with Not_found -> rt
 	  end
       | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args)
@@ -710,4 +707,4 @@ let expand_as =
   and expand_as_br map (loc,idl,cpl,rt) =
     (loc,idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
-  expand_as Idmap.empty
+  expand_as Id.Map.empty
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index 9cf83df15..55d793e03 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,12 +1,8 @@
 open Glob_term
 open Misctypes
 
-(* Ocaml 3.06 Map.S does not handle is_empty *)
-val idmap_is_empty : 'a Names.Idmap.t -> bool
-
-
 (* [get_pattern_id pat] returns a list of all the variable appearing in [pat] *)
-val get_pattern_id : cases_pattern -> Names.identifier list
+val get_pattern_id : cases_pattern -> Names.Id.t list
 
 (* [pattern_to_term pat] returns a glob_constr corresponding to [pat].
    [pat] must not contain occurences of anonymous pattern
@@ -18,7 +14,7 @@ val pattern_to_term : cases_pattern -> glob_constr
    In each of them the location is Util.Loc.ghost
 *)
 val mkGRef : Globnames.global_reference -> glob_constr
-val mkGVar : Names.identifier -> glob_constr
+val mkGVar : Names.Id.t -> glob_constr
 val mkGApp  : glob_constr*(glob_constr list) -> glob_constr
 val mkGLambda : Names.name * glob_constr * glob_constr -> glob_constr
 val mkGProd : Names.name * glob_constr * glob_constr -> glob_constr
@@ -61,7 +57,7 @@ val  glob_make_or_list : glob_constr list -> glob_constr
 
 
 (* Replace the var mapped in the glob_constr/context *)
-val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
+val change_vars : Names.Id.t Names.Id.Map.t -> glob_constr -> glob_constr
 
 
 
@@ -73,27 +69,27 @@ val change_vars : Names.identifier Names.Idmap.t -> glob_constr -> glob_constr
    [avoid] with the variables appearing in the result.
 *)
   val alpha_pat :
-    Names.Idmap.key list ->
+    Names.Id.Map.key list ->
     Glob_term.cases_pattern ->
-    Glob_term.cases_pattern * Names.Idmap.key list *
-      Names.identifier Names.Idmap.t
+    Glob_term.cases_pattern * Names.Id.Map.key list *
+      Names.Id.t Names.Id.Map.t
 
 (* [alpha_rt avoid rt] alpha convert [rt] s.t. the result repects barendregt
    conventions and  does not share bound variables with avoid
 *)
-val alpha_rt : Names.identifier list -> glob_constr -> glob_constr
+val alpha_rt : Names.Id.t list -> glob_constr -> glob_constr
 
 (* same as alpha_rt but for case branches *)
-val alpha_br : Names.identifier list ->
-    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
+val alpha_br : Names.Id.t list ->
+    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr ->
-    Loc.t * Names.identifier list * Glob_term.cases_pattern list *
+    Loc.t * Names.Id.t list * Glob_term.cases_pattern list *
     Glob_term.glob_constr
 
 
 (* Reduction function *)
 val replace_var_by_term  :
-  Names.identifier ->
+  Names.Id.t ->
   Glob_term.glob_constr -> Glob_term.glob_constr -> Glob_term.glob_constr
 
 
@@ -101,7 +97,7 @@ val replace_var_by_term  :
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
-val is_free_in : Names.identifier -> glob_constr -> bool
+val is_free_in : Names.Id.t -> glob_constr -> bool
 
 
 val are_unifiable : cases_pattern -> cases_pattern -> bool
@@ -110,13 +106,13 @@ val eq_cases_pattern : cases_pattern -> cases_pattern -> bool
 
 
 (*
-   ids_of_pat : cases_pattern -> Idset.t
+   ids_of_pat : cases_pattern -> Id.Set.t
    returns the set of variables appearing in a pattern
 *)
-val   ids_of_pat : cases_pattern -> Names.Idset.t
+val   ids_of_pat : cases_pattern -> Names.Id.Set.t
 
 (* TODO: finish this function (Fix not treated) *)
-val ids_of_glob_constr: glob_constr -> Names.Idset.t
+val ids_of_glob_constr: glob_constr -> Names.Id.Set.t
 
 (*
    removing let_in construction in a glob_constr
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 22da1a966..f922b2f60 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -85,19 +85,19 @@ let functional_induction with_clean c princl pat =
     let princ_vars =
       List.fold_right
 	(fun a acc ->
-	  try Idset.add (destVar a) acc
+	  try Id.Set.add (destVar a) acc
 	  with _ -> acc
 	)
 	args
-	Idset.empty
+	Id.Set.empty
     in
-    let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in
-    let old_idl = Idset.diff old_idl princ_vars in
+    let old_idl = List.fold_right Id.Set.add (Tacmach.pf_ids_of_hyps g) Id.Set.empty in
+    let old_idl = Id.Set.diff old_idl princ_vars in
     let subst_and_reduce g =
       if with_clean
       then
 	let idl =
-	  List.filter (fun id -> not (Idset.mem id old_idl))
+	  List.filter (fun id -> not (Id.Set.mem id old_idl))
 	    (Tacmach.pf_ids_of_hyps g)
 	in
 	let flag =
@@ -152,7 +152,7 @@ let build_newrecursive
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
+        (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
@@ -185,8 +185,8 @@ let build_newrecursive l =
 
 (* Checks whether or not the mutual bloc is recursive *)
 let is_rec names =
-  let names = List.fold_right Idset.add names Idset.empty in
-  let check_id id names =  Idset.mem id names in
+  let names = List.fold_right Id.Set.add names Id.Set.empty in
+  let check_id id names =  Id.Set.mem id names in
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
@@ -195,11 +195,11 @@ let is_rec names =
     | GIf(_,b,_,lhs,rhs) ->
 	(lookup names b) || (lookup names lhs) || (lookup names rhs)
     | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b)  ->
-	lookup names t || lookup (Nameops.name_fold Idset.remove na names) b
+	lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b
     | GLetTuple(_,nal,_,t,b) -> lookup names t ||
 	lookup
 	  (List.fold_left
-	     (fun acc na -> Nameops.name_fold Idset.remove na acc)
+	     (fun acc na -> Nameops.name_fold Id.Set.remove na acc)
 	     names
 	     nal
 	  )
@@ -209,7 +209,7 @@ let is_rec names =
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
   and lookup_br names (_,idl,_,rt) =
-    let new_names = List.fold_right Idset.remove idl names in
+    let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
   in
   lookup names
@@ -460,9 +460,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
     match wf_rel_expr_opt with 
       | None ->
 	  let ltof =
-	    let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in
+	    let make_dir l = make_dirpath (List.map Id.of_string (List.rev l)) in
 	    Libnames.Qualid (Loc.ghost,Libnames.qualid_of_path
-			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof")))
+			       (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")))
 	  in
 	  let fun_from_mes =
 	    let applied_mes =
@@ -475,8 +475,8 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas
 	  wf_rel_from_mes,true
       | Some wf_rel_expr -> 
 	  let wf_rel_with_mes = 
-	    let a = Names.id_of_string "___a" in 
-	    let b = Names.id_of_string "___b" in 
+	    let a = Names.Id.of_string "___a" in 
+	    let b = Names.Id.of_string "___b" in 
 	    Constrexpr_ops.mkLambdaC(
 	      [Loc.ghost,Name a;Loc.ghost,Name b],
 	      Constrexpr.Default Explicit,
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index fb9116cc2..2d50adf00 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -4,7 +4,7 @@ open Libnames
 open Globnames
 open Refiner
 open Hiddentac 
-let mk_prefix pre id = id_of_string (pre^(string_of_id id))
+let mk_prefix pre id = Id.of_string (pre^(Id.to_string id))
 let mk_rel_id = mk_prefix "R_"
 let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
 let mk_complete_id id = Nameops.add_suffix (mk_rel_id id) "_complete"
@@ -16,7 +16,7 @@ let msgnl m =
 let invalid_argument s = raise (Invalid_argument s)
 
 
-let fresh_id avoid s = Namegen.next_ident_away_in_goal (id_of_string s) avoid
+let fresh_id avoid s = Namegen.next_ident_away_in_goal (Id.of_string s) avoid
 
 let fresh_name avoid s = Name (fresh_id avoid s)
 
@@ -116,7 +116,7 @@ let const_of_id id =
     qualid_of_reference (Libnames.Ident (Loc.ghost,id))
   in
   try Nametab.locate_constant princ_ref
-  with Not_found -> Errors.error ("cannot find "^ string_of_id id)
+  with Not_found -> Errors.error ("cannot find "^ Id.to_string id)
 
 let def_of_const t =
    match (Term.kind_of_term t) with
@@ -133,8 +133,8 @@ let coq_constant s =
 
 let find_reference sl s =
     (Nametab.locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 
 let eq = lazy(coq_constant "eq")
 let refl_equal = lazy(coq_constant "eq_refl")
@@ -510,8 +510,8 @@ let jmeq_refl () =
 let h_intros l =
   tclMAP h_intro l
 
-let h_id = id_of_string "h"
-let hrec_id = id_of_string "hrec"
+let h_id = Id.of_string "h"
+let hrec_id = Id.of_string "hrec"
 let well_founded = function () -> (coq_constant "well_founded")
 let acc_rel = function () -> (coq_constant "Acc")
 let acc_inv_id = function () -> (coq_constant "Acc_inv")
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 8f80c072c..7d0f5a00e 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -5,23 +5,23 @@ open Pp
    The mk_?_id function build different name w.r.t. a function
    Each of their use is justified in the code
 *)
-val mk_rel_id : identifier -> identifier
-val mk_correct_id : identifier -> identifier
-val mk_complete_id : identifier -> identifier
-val mk_equation_id : identifier -> identifier
+val mk_rel_id : Id.t -> Id.t
+val mk_correct_id : Id.t -> Id.t
+val mk_complete_id : Id.t -> Id.t
+val mk_equation_id : Id.t -> Id.t
 
 
 val msgnl : std_ppcmds -> unit
 
 val invalid_argument : string -> 'a
 
-val fresh_id : identifier list -> string -> identifier
-val fresh_name : identifier list -> string -> name
-val get_name : identifier list -> ?default:string -> name -> name
+val fresh_id : Id.t list -> string -> Id.t
+val fresh_name : Id.t list -> string -> name
+val get_name : Id.t list -> ?default:string -> name -> name
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : name -> identifier
+val id_of_name : name -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
 val locate_constant : Libnames.reference -> constant
@@ -44,7 +44,7 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 val def_of_const : Term.constr -> Term.constr
 val eq : Term.constr Lazy.t
 val refl_equal : Term.constr Lazy.t
-val const_of_id: identifier -> constant
+val const_of_id: Id.t -> constant
 val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
@@ -54,14 +54,14 @@ val jmeq_refl : unit -> Term.constr
 
 val new_save_named : bool -> unit
 
-val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
+val save : bool -> Id.t ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Tacexpr.declaration_hook -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
 *)
 val get_proof_clean : bool ->
-  Names.identifier *
+  Names.Id.t *
     (Entries.definition_entry * Decl_kinds.goal_kind *
       unit Tacexpr.declaration_hook)
 
@@ -113,9 +113,9 @@ exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
 
-val h_intros: Names.identifier list -> Proof_type.tactic
-val h_id :  Names.identifier
-val hrec_id :  Names.identifier
+val h_intros: Names.Id.t list -> Proof_type.tactic
+val h_id :  Names.Id.t
+val hrec_id :  Names.Id.t
 val acc_inv_id :  Term.constr Util.delayed
 val ltof_ref : Globnames.global_reference Util.delayed
 val well_founded_ltof : Term.constr Util.delayed
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 517a1ce9c..4a466175f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -126,8 +126,8 @@ let generate_type g_to_f f graph i =
   (*i We need to name the vars [res] and [fv] i*)
   let filter = function (Name id,_,_) -> Some id | (Anonymous,_,_) -> None in
   let named_ctxt = List.map_filter filter fun_ctxt in
-  let res_id = Namegen.next_ident_away_in_goal (id_of_string "_res") named_ctxt in
-  let fv_id = Namegen.next_ident_away_in_goal (id_of_string "fv") (res_id :: named_ctxt) in
+  let res_id = Namegen.next_ident_away_in_goal (Id.of_string "_res") named_ctxt in
+  let fv_id = Namegen.next_ident_away_in_goal (Id.of_string "fv") (res_id :: named_ctxt) in
   (*i we can then type the argument to be applied to the function [f] i*)
   let args_as_rels = Array.of_list (args_from_decl 1 [] fun_ctxt) in
   (*i
@@ -242,13 +242,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easilly computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the funcitonnal principle is defined in the
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -258,7 +258,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroIdentifier id)
-	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
@@ -276,16 +276,16 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_right
 	(fun (_,pat) acc ->
 	     match pat with
-	       | Genarg.IntroIdentifier id -> Idset.add id acc
+	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
 	| _ -> anomaly "Not an identifier"
 	)
 	(List.nth intro_pats (pred i))
-	Idset.empty
+	Id.Set.empty
       in
 	let pre_args g =
 	List.fold_right
 	  (fun (id,b,t) pre_args ->
-	    if Idset.mem id this_branche_ids
+	    if Id.Set.mem id this_branche_ids
 	    then
 	      match b with
 		| None -> id::pre_args
@@ -299,7 +299,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let pre_tac g =
 	List.fold_right
 	  (fun (id,b,t) pre_tac ->
-	     if Idset.mem id this_branche_ids
+	     if Id.Set.mem id this_branche_ids
 	     then
 	       match b with
 		 | None -> pre_tac
@@ -383,7 +383,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let app_constructor g = applist((mkConstruct(constructor)),constructor_args g) in
       (* an apply the tactic *)
       let res,hres =
-	match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
 	  | [res;hres] -> res,hres
 	  | _ -> assert false
       in
@@ -466,7 +466,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	  princ_type
 	  (h_exact f_principle));
 	observe_tac "intro args_names" (tclMAP h_intro args_names);
-	(* observe_tac "titi" (pose_proof (Name (id_of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
+	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
@@ -506,13 +506,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easilly computable *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the funcitonnal principle is defined in the
        environement and due to the bug #1174, we will need to pose the principle
        using a name
     *)
-    let principle_id = Namegen.next_ident_away_in_goal (id_of_string "princ") ids in
+    let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in
     let ids = principle_id :: ids in
     (* We get the branches of the principle *)
     let branches = List.rev princ_infos.branches in
@@ -522,7 +522,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> Loc.ghost, Genarg.IntroIdentifier id)
-	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
@@ -540,17 +540,17 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
 	List.fold_right
 	  (fun (_,pat) acc ->
 	     match pat with
-	       | Genarg.IntroIdentifier id -> Idset.add id acc
+	       | Genarg.IntroIdentifier id -> Id.Set.add id acc
 	       | _ -> anomaly "Not an identifier"
 	  )
 	  (List.nth intro_pats (pred i))
-	  Idset.empty
+	  Id.Set.empty
       in
       (* and get the real args of the branch by unfolding the defined constant *)
       let pre_args,pre_tac =
 	List.fold_right
 	  (fun (id,b,t) (pre_args,pre_tac) ->
-	     if Idset.mem id this_branche_ids
+	     if Id.Set.mem id this_branche_ids
 	     then
 	       match b with
 		 | None -> (id::pre_args,pre_tac)
@@ -624,7 +624,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       let app_constructor = applist((mkConstruct(constructor)),constructor_args) in
       (* an apply the tactic *)
       let res,hres =
-	match generate_fresh_id (id_of_string "z") (ids(* @this_branche_ids *)) 2 with
+	match generate_fresh_id (Id.of_string "z") (ids(* @this_branche_ids *)) 2 with
 	  | [res;hres] -> res,hres
 	  | _ -> assert false
       in
@@ -735,7 +735,7 @@ and intros_with_rewrite_aux : tactic =
 		  | App(eq,args) when (eq_constr eq eq_ind)  ->
  		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id; thin [id]; intros_with_rewrite ] g
 		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
@@ -753,7 +753,7 @@ and intros_with_rewrite_aux : tactic =
 		      ] g
 		      else if isVar args.(1)
 		      then
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id;
 				     generalize_dependent_of (destVar args.(1)) id;
 				     tclTRY (Equality.rewriteLR (mkVar id));
@@ -762,7 +762,7 @@ and intros_with_rewrite_aux : tactic =
 			  g
 		      else if isVar args.(2) 
 		      then 
-			let id = pf_get_new_id (id_of_string "y") g  in
+			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ h_intro id;
 				     generalize_dependent_of (destVar args.(2)) id;
 				     tclTRY (Equality.rewriteRL (mkVar id));
@@ -771,7 +771,7 @@ and intros_with_rewrite_aux : tactic =
 			  g
 		      else
 			begin
-			  let id = pf_get_new_id (id_of_string "y") g  in
+			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
 			    h_intro id;
 			    tclTRY (Equality.rewriteLR (mkVar id));
@@ -797,7 +797,7 @@ and intros_with_rewrite_aux : tactic =
 			intros_with_rewrite
 		      ] g
 		  | _ ->
-		      let id = pf_get_new_id (id_of_string "y") g  in
+		      let id = pf_get_new_id (Id.of_string "y") g  in
 		      tclTHENSEQ [ h_intro id;intros_with_rewrite] g
 	      end
 	  | LetIn _ ->
@@ -904,11 +904,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
        and compute a fresh name for each of them
     *)
     let nb_fun_args = nb_prod (pf_concl g)  - 2  in
-    let args_names = generate_fresh_id (id_of_string "x") [] nb_fun_args in
+    let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
     let res,hres,graph_principle_id =
-      match generate_fresh_id (id_of_string "z") ids 3 with
+      match generate_fresh_id (Id.of_string "z") ids 3 with
 	| [res;hres;graph_principle_id] -> res,hres,graph_principle_id
 	| _ -> assert false
     in
@@ -920,7 +920,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun (_,_,br_type) ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (id_of_string "y") ids (nb_prod br_type))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod br_type))
 	)
 	branches
     in
@@ -1059,7 +1059,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove correctness ("^(string_of_id f_id)^")")
+	   (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
@@ -1110,7 +1110,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
 	   (fst lemmas_types_infos.(i))
 	   (fun _ _ -> ());
 	 Pfedit.by
-	   (observe_tac ("prove completeness ("^(string_of_id f_id)^")")
+	   (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i));
 	 do_save ();
 	 let finfo = find_Function_infos f_as_constant in
@@ -1187,7 +1187,7 @@ let revert_graph kn post_tac hid g =
 
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
-    let old_ids = List.fold_right Idset.add  (pf_ids_of_hyps g) Idset.empty in
+    let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let type_of_h = pf_type_of g (mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (Coqlib.build_coq_eq ())  ->
@@ -1206,7 +1206,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_intro hid;
 	    Inv.inv FullInversion None (NamedHyp hid);
 	    (fun g ->
-	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in
+	       let new_ids = List.filter (fun id -> not (Id.Set.mem id old_ids)) (pf_ids_of_hyps g) in
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
 	    );
 	  ] g
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 485b5b280..089493079 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -53,10 +53,10 @@ let understand = Pretyping.understand Evd.empty (Global.env())
 
 (** Operations on names and identifiers *)
 let id_of_name = function
-    Anonymous -> id_of_string "H"
+    Anonymous -> Id.of_string "H"
   | Name id   -> id;;
-let name_of_string str = Name (id_of_string str)
-let string_of_name nme = string_of_id (id_of_name nme)
+let name_of_string str = Name (Id.of_string str)
+let string_of_name nme = Id.to_string (id_of_name nme)
 
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
@@ -75,7 +75,7 @@ let ident_global_exist id =
 
 (** [next_ident_fresh id] returns a fresh identifier (ie not linked in
     global env) with base [id]. *)
-let next_ident_fresh (id:identifier) =
+let next_ident_fresh (id:Id.t) =
     let res = ref id in
     while ident_global_exist !res do res := Nameops.lift_subscript !res done;
     !res
@@ -129,7 +129,7 @@ let prNamedRLDecl s lc =
     prstr "\n";
   end
 
-let showind (id:identifier) =
+let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
   let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) ind1 in
@@ -247,7 +247,7 @@ type 'a merged_arg =
 
 type merge_infos =
     {
-      ident:identifier; (** new inductive name *)
+      ident:Id.t; (** new inductive name *)
       mib1: mutual_inductive_body;
       oib1: one_inductive_body;
       mib2: mutual_inductive_body;
@@ -350,8 +350,8 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
 
 (** {1 Utilities for merging} *)
 
-let ind1name = id_of_string "__ind1"
-let ind2name = id_of_string "__ind2"
+let ind1name = Id.of_string "__ind1"
+let ind2name = Id.of_string "__ind2"
 
 (** Performs verifications on two graphs before merging: they must not
     be co-inductive, and for the moment they must not be mutual
@@ -374,11 +374,11 @@ let build_raw_params prms_decl avoid =
   let _ = prNamedRConstr "RAWDUMMY" dummy_glob_constr in
   let res,_ = glob_decompose_prod dummy_glob_constr in
   let comblist = List.combine prms_decl res in
-  comblist, res , (avoid @ (Idset.elements (ids_of_glob_constr dummy_glob_constr)))
+  comblist, res , (avoid @ (Id.Set.elements (ids_of_glob_constr dummy_glob_constr)))
 *)
 
 let ids_of_rawlist avoid rawl =
-    List.fold_left Idset.union avoid (List.map ids_of_glob_constr rawl)
+    List.fold_left Id.Set.union avoid (List.map ids_of_glob_constr rawl)
 
 
 
@@ -456,7 +456,7 @@ let shift_linked_params mib1 mib2 (lnk1:linked_var array) (lnk2:linked_var array
       ([],[],[],[]) arity_ctxt in
 (*  let arity_ctxt2 =
     build_raw_params oib2.mind_arity_ctxt
-      (Idset.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
+      (Id.Set.elements (ids_of_glob_constr oib1.mind_arity_ctxt)) in*)
   let recprms1,otherprms1,args1,funresprms1 = bldprms (List.rev oib1.mind_arity_ctxt) mlnk1 in
   let _ = prstr "\n\n\n" in
   let recprms2,otherprms2,args2,funresprms2 = bldprms (List.rev oib2.mind_arity_ctxt) mlnk2 in
@@ -564,7 +564,7 @@ let build_suppl_reccall (accrec:(name * glob_constr) list) concl2 shift =
   List.map (fun (nm,tp) -> (nm,merge_app_unsafe tp concl2 shift)) accrec
 
 
-let find_app (nme:identifier) ltyp =
+let find_app (nme:Id.t) ltyp =
   try
     ignore
       (List.map
@@ -650,16 +650,16 @@ let rec merge_types shift accrec1
     linked args [allargs2] to target args of [allargs1] as specified
     in [shift]. [allargs1] and [allargs2] are in reverse order.  Also
     returns the list of unlinked vars of [allargs2]. *)
-let build_link_map_aux (allargs1:identifier array) (allargs2:identifier array)
+let build_link_map_aux (allargs1:Id.t array) (allargs2:Id.t array)
     (lnk:int merged_arg array) =
   Array.fold_left_i
     (fun i acc e ->
       if i = Array.length lnk - 1 then acc (* functional arg, not in allargs *)
       else
         match e with
-          | Prm_linked j | Arg_linked j -> Idmap.add allargs2.(i) allargs1.(j) acc
+          | Prm_linked j | Arg_linked j -> Id.Map.add allargs2.(i) allargs1.(j) acc
           | _ -> acc)
-    Idmap.empty lnk
+    Id.Map.empty lnk
 
 let build_link_map allargs1 allargs2 lnk =
   let allargs1 =
@@ -742,18 +742,18 @@ let fresh_cstror_suffix , cstror_suffix_init =
 (** [merge_constructor_id id1 id2 shift] returns the identifier of the
     new constructor from the id of the two merged constructor and
     the merging info. *)
-let merge_constructor_id id1 id2 shift:identifier =
-  let id = string_of_id shift.ident ^ "_" ^ fresh_cstror_suffix () in
-  next_ident_fresh (id_of_string id)
+let merge_constructor_id id1 id2 shift:Id.t =
+  let id = Id.to_string shift.ident ^ "_" ^ fresh_cstror_suffix () in
+  next_ident_fresh (Id.of_string id)
 
 
 
 (** [merge_constructors lnk shift avoid] merges the two list of
     constructor [(name*type)]. These are translated to glob_constr
     first, each of them having distinct var names. *)
-let merge_constructors (shift:merge_infos) (avoid:Idset.t)
-    (typcstr1:(identifier * glob_constr) list)
-    (typcstr2:(identifier * glob_constr) list) : (identifier * glob_constr) list =
+let merge_constructors (shift:merge_infos) (avoid:Id.Set.t)
+    (typcstr1:(Id.t * glob_constr) list)
+    (typcstr2:(Id.t * glob_constr) list) : (Id.t * glob_constr) list =
   List.flatten
     (List.map
         (fun (id1,rawtyp1) ->
@@ -775,14 +775,14 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
-    Detyping.detype false (Idset.elements avoid) [] substindtyp in
+    Detyping.detype false (Id.Set.elements avoid) [] substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
-  let avoid2 = Idset.union avoid (ids_of_rawlist avoid lcstr1) in
+  let avoid2 = Id.Set.union avoid (ids_of_rawlist avoid lcstr1) in
   let lcstr2 =
     Array.to_list (Array.map (mkrawcor ind2name avoid2) oib2.mind_user_lc) in
-  let avoid3 = Idset.union avoid (ids_of_rawlist avoid lcstr2) in
+  let avoid3 = Id.Set.union avoid (ids_of_rawlist avoid lcstr2) in
 
   let params1 =
     try fst (glob_decompose_prod_n shift.nrecprms1 (List.hd lcstr1))
@@ -806,11 +806,11 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
 let merge_mutual_inductive_body
     (mib1:mutual_inductive_body) (mib2:mutual_inductive_body) (shift:merge_infos) =
   (* Mutual not treated, we take first ind body of each. *)
-  merge_inductive_body shift Idset.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
+  merge_inductive_body shift Id.Set.empty mib1.mind_packets.(0) mib2.mind_packets.(0)
 
 
 let glob_constr_to_constr_expr x = (* build a constr_expr from a glob_constr *)
-  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Idset.empty) x
+  Flags.with_option Flags.raw_print (Constrextern.extern_glob_type Id.Set.empty) x
 
 let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
   let params = prms2 @ prms1 in
@@ -842,7 +842,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
 let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(identifier * glob_constr) list) =
+    (rawlist:(Id.t * glob_constr) list) =
   let lident = Loc.ghost, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
@@ -875,7 +875,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
   let prms1,prms2, rawlist = merge_mutual_inductive_body mib1 mib2 shift_prm in
   let _ = prstr "\nrawlist : " in
   let _ =
-    List.iter (fun (nm,tp) -> prNamedRConstr (string_of_id nm) tp;prstr "\n") rawlist in
+    List.iter (fun (nm,tp) -> prNamedRConstr (Id.to_string nm) tp;prstr "\n") rawlist in
   let _ = prstr "\nend rawlist\n" in
 (* FIX: retransformer en constr ici
    let shift_prm =
@@ -892,7 +892,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
 
 
 (* Find infos on identifier id. *)
-let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
+let find_Function_infos_safe (id:Id.t): Indfun_common.function_info =
   let kn_of_id x =
     let f_ref = Libnames.Ident (Loc.ghost,x) in
     locate_with_msg (str "Don't know what to do with " ++ Libnames.pr_reference f_ref)
@@ -909,8 +909,8 @@ let find_Function_infos_safe (id:identifier): Indfun_common.function_info =
 
     Warning: For the moment, repetitions of an id in [args1] or
     [args2] are not supported. *)
-let merge (id1:identifier) (id2:identifier) (args1:identifier array)
-    (args2:identifier array) id : unit =
+let merge (id1:Id.t) (id2:Id.t) (args1:Id.t array)
+    (args2:Id.t array) id : unit =
   let finfo1 = find_Function_infos_safe id1 in
   let finfo2 = find_Function_infos_safe id2 in
   (* FIXME? args1 are supposed unlinked. mergescheme (G x x) ?? *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index a2f16dc6d..28752fe4f 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -51,11 +51,11 @@ let coq_base_constant s =
 
 let find_reference sl s =
     (locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 
 
-let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
+let (declare_fun : Id.t -> logical_kind -> constr -> global_reference) =
   fun f_id kind value ->
     let ce = {const_entry_body = value;
               const_entry_secctx = None;
@@ -73,7 +73,7 @@ let def_of_const t =
 	     | _ -> assert false)
        with _ ->
 	 anomaly ("Cannot find definition of constant "^
-		    (string_of_id (id_of_label (con_label sp))))
+		    (Id.to_string (id_of_label (con_label sp))))
       )
      |_ -> assert false
 
@@ -86,8 +86,8 @@ let type_of_const t =
 let constant sl s =
   constr_of_global
     (locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
+			   (List.map Id.of_string (List.rev sl)))
+	       (Id.of_string s)));;
 let const_of_ref = function
     ConstRef kn -> kn
   | _ -> anomaly "ConstRef expected"
@@ -120,15 +120,15 @@ let pf_get_new_ids idl g =
 let compute_renamed_type gls c =
   rename_bound_vars_as_displayed (*no avoid*) [] (*no rels*) []
     (pf_type_of gls c)
-let h'_id = id_of_string "h'"
-let teq_id = id_of_string "teq"
-let ano_id = id_of_string "anonymous"
-let x_id = id_of_string "x"
-let k_id = id_of_string "k"
-let v_id = id_of_string "v"
-let def_id = id_of_string "def"
-let p_id = id_of_string "p"
-let rec_res_id = id_of_string "rec_res";;
+let h'_id = Id.of_string "h'"
+let teq_id = Id.of_string "teq"
+let ano_id = Id.of_string "anonymous"
+let x_id = Id.of_string "x"
+let k_id = Id.of_string "k"
+let v_id = Id.of_string "v"
+let def_id = Id.of_string "def"
+let p_id = Id.of_string "p"
+let rec_res_id = Id.of_string "rec_res";;
 let lt = function () -> (coq_base_constant "lt")
 let le = function () -> (coq_base_constant "le")
 let ex = function () -> (coq_base_constant "ex")
@@ -202,7 +202,7 @@ let (value_f:constr list -> global_reference -> constr) =
     let body = understand Evd.empty env glob_body in
     it_mkLambda_or_LetIn body context
 
-let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
+let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> global_reference) =
   fun f_id kind input_type fterm_ref ->
     declare_fun f_id kind (value_f input_type fterm_ref);;
 
@@ -300,7 +300,7 @@ let check_not_nested forbidden e =
   let rec check_not_nested e =  
     match kind_of_term e with 
       | Rel _ -> ()
-      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^string_of_id x)
+      | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^Id.to_string x)
       | Meta _ | Evar _ | Sort _ -> ()
       | Cast(e,_,t) -> check_not_nested e;check_not_nested t
       | Prod(_,t,b) -> check_not_nested t;check_not_nested b
@@ -324,21 +324,21 @@ let check_not_nested forbidden e =
 type 'a infos = 
     { nb_arg : int; (* function number of arguments *)
       concl_tac : tactic; (* final tactic to finish proofs *)
-      rec_arg_id : identifier; (*name of the declared recursive argument *)
+      rec_arg_id : Id.t; (*name of the declared recursive argument *)
       is_mes : bool; (* type of recursion *)
-      ih : identifier; (* induction hypothesis name *)
-      f_id : identifier;  (* function name *)
+      ih : Id.t; (* induction hypothesis name *)
+      f_id : Id.t;  (* function name *)
       f_constr : constr;  (* function term *)
       f_terminate : constr; (* termination proof term *)
       func : global_reference; (* functionnal reference *)
       info : 'a;
       is_main_branch : bool; (* on the main branch or on a matched expression *)
       is_final : bool; (* final first order term or not *)
-      values_and_bounds : (identifier*identifier) list; 
-      eqs : identifier list; 
-      forbidden_ids : identifier list;
+      values_and_bounds : (Id.t*Id.t) list; 
+      eqs : Id.t list; 
+      forbidden_ids : Id.t list;
       acc_inv : constr lazy_t;
-      acc_id : identifier;
+      acc_id : Id.t;
       args_assoc : ((constr list)*constr) list;
     }
 
@@ -651,7 +651,7 @@ let terminate_letin (na,b,t,e) expr_info continuation_tac info =
   introduced back later; the result is the pair of the tactic and the
   list of hypotheses that have been generalized and cleared. *)
 let mkDestructEq :
-  identifier list -> constr -> goal sigma -> tactic * identifier list =
+  Id.t list -> constr -> goal sigma -> tactic * Id.t list =
   fun not_on_hyp expr g ->
   let hyps = pf_hyps g in
   let to_revert =
@@ -1031,10 +1031,10 @@ let termination_proof_header is_mes input_type ids args_id relation
       in
       let relation = substl pre_rec_args relation in
       let input_type = substl pre_rec_args input_type in
-      let wf_thm = next_ident_away_in_goal (id_of_string ("wf_R")) ids in
+      let wf_thm = next_ident_away_in_goal (Id.of_string ("wf_R")) ids in
       let wf_rec_arg =
 	next_ident_away_in_goal
-	  (id_of_string ("Acc_"^(string_of_id rec_arg_id)))
+	  (Id.of_string ("Acc_"^(Id.to_string rec_arg_id)))
 	  (wf_thm::ids)
       in
       let hrec = next_ident_away_in_goal hrec_id
@@ -1206,8 +1206,8 @@ let build_and_l l =
 
 
 let is_rec_res id =
-  let rec_res_name = string_of_id rec_res_id   in
-  let id_name = string_of_id id in
+  let rec_res_name = Id.to_string rec_res_id   in
+  let id_name = Id.to_string id in
   try
     String.sub id_name 0 (String.length rec_res_name) = rec_res_name
   with _ -> false
@@ -1384,7 +1384,7 @@ let com_terminate
 
 
 let start_equation (f:global_reference) (term_f:global_reference)
-  (cont_tactic:identifier list -> tactic) g =
+  (cont_tactic:Id.t list -> tactic) g =
   let ids = pf_ids_of_hyps g in
   let terminate_constr = constr_of_global term_f in
   let nargs = nb_prod (type_of_const terminate_constr) in
@@ -1397,7 +1397,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
                              Array.of_list (List.map mkVar x))));
     observe_tac (str "prove_eq") (cont_tactic x)] g;;
 
-let (com_eqn : int -> identifier ->
+let (com_eqn : int -> Id.t ->
        global_reference -> global_reference -> global_reference
 	 -> constr -> unit) =
   fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type ->
@@ -1430,12 +1430,12 @@ let (com_eqn : int -> identifier ->
 		eqs = [];
 		forbidden_ids = [];
 		acc_inv = lazy (assert false);
-		acc_id = id_of_string "____";
+		acc_id = Id.of_string "____";
 		args_assoc = [];
-		f_id = id_of_string "______";
-		rec_arg_id = id_of_string "______";
+		f_id = Id.of_string "______";
+		rec_arg_id = Id.of_string "______";
 		is_mes = false;
-		ih = id_of_string "______";
+		ih = Id.of_string "______";
 	       }
 	  )
        ); 
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index 1117e2597..2ef685203 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -4,11 +4,11 @@
 val tclUSER_if_not_mes : 
   Proof_type.tactic ->
   bool -> 
-  Names.identifier list option -> 
+  Names.Id.t list option -> 
   Proof_type.tactic
 val recursive_definition :  
 bool ->
-           Names.identifier ->
+           Names.Id.t ->
            Constrintern.internalization_env ->
            Constrexpr.constr_expr ->
            Constrexpr.constr_expr ->