Modulification of identifier

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

1 files changed, 14 insertions, 14 deletions

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