diff options
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 0b8cbf6dc5..fff4711044 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -85,7 +85,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 |