diff options
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 87d646ab89..6f6607fccc 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -111,6 +111,7 @@ val pr_table : unit -> Pp.std_ppcmds (* val function_debug : bool ref *) val do_observe : unit -> bool +val do_rewrite_dependent : unit -> bool (* To localize pb *) exception Building_graph of exn |