1 files changed, 17 insertions, 15 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index a95b1242ac..550f727951 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -9,9 +9,6 @@ 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 : Pp.t -> unit
-
 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
@@ -38,18 +35,9 @@ val chop_rprod_n : int -> Glob_term.glob_constr ->
 
 val eq : EConstr.constr Lazy.t
 val refl_equal : EConstr.constr Lazy.t
-val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
-
-val save
-  :  Id.t
-  -> Evd.side_effects Proof_global.proof_entry
-  -> ?hook:DeclareDef.Hook.t
-  -> UState.t
-  -> DeclareDef.locality
-  -> Decls.logical_kind
-  -> unit
+val make_eq : unit -> EConstr.constr
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
@@ -74,8 +62,8 @@ type function_info =
       is_general : bool;
     }
 
-val find_Function_infos : Constant.t -> function_info
-val find_Function_of_graph : inductive -> function_info
+val find_Function_infos : Constant.t -> function_info option
+val find_Function_of_graph : inductive -> function_info option
 (* WARNING: To be used just after the graph definition !!! *)
 val add_Function : bool -> Constant.t -> unit
 val update_Function : function_info -> unit
@@ -84,7 +72,21 @@ val update_Function : function_info -> unit
 val pr_info : Environ.env -> Evd.evar_map -> function_info -> Pp.t
 val pr_table : Environ.env -> Evd.evar_map -> Pp.t
 
+val observe_tac
+  : (Environ.env -> Evd.evar_map -> Pp.t)
+  -> Tacmach.tactic -> Tacmach.tactic
+
+module New : sig
+
+  val observe_tac
+    : header:Pp.t
+    -> (Environ.env -> Evd.evar_map -> Pp.t)
+    -> unit Proofview.tactic -> unit Proofview.tactic
+
+end
+
 (* val function_debug : bool ref  *)
+val observe : Pp.t -> unit
 val do_observe : unit -> bool
 val do_rewrite_dependent : unit -> bool