aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
authorMaxime Dénès2017-07-31 15:26:39 +0200
committerMaxime Dénès2017-07-31 15:26:39 +0200
commit2f349829c125ed0e2d55548935e7b90e7719f12e (patch)
tree2d3003a0072af5ab5f1268c1570b2d83ead70060 /plugins/cc
parent9a872809b246bb6af0c177d530581f7c0c36583f (diff)
parente3c247c1d96f39d2c07d120b69598a904b7d9f19 (diff)
Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index e6abf1ccf0..f904aa3e68 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 : (unit -> Pp.std_ppcmds) -> unit
+val debug : (unit -> Pp.t) -> unit
val forest : state -> forest
@@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list
val execute : bool -> state -> explanation option
-val pr_idx_term : forest -> int -> Pp.std_ppcmds
+val pr_idx_term : forest -> int -> Pp.t
val empty_forest: unit -> forest