diff options
| author |  Daniel de Rauglaudre <daniel.de_rauglaudre@inria.fr> | 2016-04-08 14:53:32 +0200 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-04-08 14:58:42 +0200 |
| commit | 17c9a9775e99d1551bf6d346d731271e3ae34417 (patch) | |
| tree | 04c63b6dded7381b61a8d915fd486744967efefd /plugins/cc/ccalgo.mli | |
| parent | 9f0a896536e709880de5ba638069dea680803f62 (diff) | |
Fixing a source of inefficiency and an artificial dependency in the
printer in the congruence tactic.
Debugging messages were always built even when not in the verbose mode
of congruence.
Diffstat (limited to 'plugins/cc/ccalgo.mli')
| -rw-r--r-- | plugins/cc/ccalgo.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index b73c8eef8..c7fa2f56f 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -120,7 +120,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : Pp.std_ppcmds -> unit +val debug : (unit -> Pp.std_ppcmds) -> unit val forest : state -> forest |