diff options
| author | Emilio Jesus Gallego Arias | 2019-07-17 16:33:41 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-31 11:13:04 +0200 |
| commit | fac3d5e2159ddafb947448ee42aa892325f320ee (patch) | |
| tree | a8737f5227bf2836107dfece63aef8b1c004c950 /plugins/funind/indfun_common.mli | |
| parent | ce22c1cb3bca8381d9b0ebfef2fbf27e92418b0c (diff) | |
[funind] Move duplicated `observe_tac` function to indfun_common.
We also attempt a version that may work with `Proofview.tactic` , may
need more work.
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 |