1 files changed, 64 insertions, 0 deletions
diff --git a/contrib/funind/indfun_common.mli b/contrib/funind/indfun_common.mli
index ab5195b0..00e1ce8d 100644
--- a/contrib/funind/indfun_common.mli
+++ b/contrib/funind/indfun_common.mli
@@ -1,7 +1,15 @@
 open Names
 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 msgnl : std_ppcmds -> unit
 
@@ -39,3 +47,59 @@ val refl_equal : Term.constr Lazy.t
 val const_of_id: identifier -> constant
 
 
+(* [save_named] is a copy of [Command.save_named] but uses 
+   [nf_betaiotazeta] instead of [nf_betaiotaevar_preserving_vm_cast] 
+   
+
+
+   DON'T USE IT if you cannot ensure that there is no VMcast in the proof
+
+*)
+
+(* val nf_betaiotazeta : Reductionops.reduction_function *)
+
+val new_save_named : bool -> unit 
+
+val save : bool -> identifier ->  Entries.definition_entry  -> Decl_kinds.goal_kind -> 
+  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 *
+    (Entries.definition_entry * Decl_kinds.goal_kind *
+       Tacexpr.declaration_hook)
+    
+
+
+
+(*****************)
+
+type function_info = 
+    { 
+      function_constant : constant;
+      graph_ind : inductive;
+      equation_lemma : constant option;
+      correctness_lemma : constant option;
+      completeness_lemma : constant option;
+      rect_lemma : constant option;
+      rec_lemma : constant option;
+      prop_lemma : constant option;
+    }
+
+val find_Function_infos : constant -> function_info
+val find_Function_of_graph : inductive -> function_info
+(* WARNING: To be used just after the graph definition !!! *)
+val add_Function : constant -> unit
+
+val update_Function : function_info -> unit 
+
+
+(** debugging *) 
+val pr_info : function_info -> Pp.std_ppcmds
+val pr_table : unit -> Pp.std_ppcmds
+
+
+val function_debug : bool ref 
+val do_observe : unit -> bool