aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/ccalgo.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-06-20 08:09:00 +0200
committerMaxime Dénès2017-06-20 08:09:00 +0200
commit25cd7acea0df79fcc07274e429c9839de1246611 (patch)
tree1ee95df49ec9ea7152afed41df425ea4e4760736 /plugins/cc/ccalgo.mli
parentc7ac5dc8036623a02ab4ad6d11469e040e78c004 (diff)
parent0437339ccac602d692b5b8c071b77ac756805520 (diff)
Merge PR#803: Clean ssr
Diffstat (limited to 'plugins/cc/ccalgo.mli')
-rw-r--r--plugins/cc/ccalgo.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 505029992a..51e2301fe6 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -129,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t
val epsilons : forest -> pa_constructor list
-val empty : int -> Proof_type.goal Evd.sigma -> state
+val empty : int -> Goal.goal Evd.sigma -> state
val add_term : state -> term -> int