1 files changed, 27 insertions, 25 deletions

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e0076735..67ddf374 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -5,23 +5,21 @@ 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.t
+val get_name : Id.t list -> ?default:string -> Name.t -> Name.t
 
 val array_get_start : 'a array -> 'a array
 
-val id_of_name : name -> identifier
+val id_of_name : Name.t -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
 val locate_constant : Libnames.reference -> constant
@@ -36,38 +34,31 @@ val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
 val chop_rlambda_n : int -> Glob_term.glob_constr ->
-  (name*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
 
 val chop_rprod_n : int -> Glob_term.glob_constr ->
-  (name*Glob_term.glob_constr) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr) list * 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
 
-(* [save_named] is a copy of [Command.save_named] but uses
-   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast]
-*)
-
-val new_save_named : bool -> unit
-
-val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  Tacexpr.declaration_hook -> unit
+val save : bool -> Id.t -> Entries.definition_entry  -> Decl_kinds.goal_kind ->
+  unit Lemmas.declaration_hook Ephemeron.key -> 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 *
-    (Entries.definition_entry * Decl_kinds.goal_kind *
-       Tacexpr.declaration_hook)
+  Names.Id.t *
+    (Entries.definition_entry * Decl_kinds.goal_kind)
 
 
 
-(* [with_full_print f a] applies [f] to [a] in full printing environment
+(* [with_full_print f a] applies [f] to [a] in full printing environment.
 
    This function preserves the print settings
 *)
@@ -112,3 +103,14 @@ exception Defining_principle of exn
 exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
+
+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
+val acc_rel : Term.constr Util.delayed
+val well_founded : Term.constr Util.delayed
+val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
+val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic