aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc/ccalgo.mli
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-13 17:13:44 +0100
committerMaxime Dénès2017-11-13 17:13:44 +0100
commit8d176db01baf9fb4a5e07decb9500ef4a8717e93 (patch)
tree675b02e411ff2c56a9aff39f4956a055eac254a7 /plugins/cc/ccalgo.mli
parent29a7307ea7cd36408661ba633a235793f11dca84 (diff)
parent03e21974a3e971a294533bffb81877dc1bd270b6 (diff)
Merge PR #6098: [api] Move structures deprecated in the API to the core.
Diffstat (limited to 'plugins/cc/ccalgo.mli')
-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 f904aa3e68..23cd2161d7 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -7,7 +7,7 @@
(************************************************************************)
open Util
-open Term
+open Constr
open Names
type pa_constructor =
@@ -85,7 +85,7 @@ type representative=
mutable lfathers:Int.Set.t;
mutable fathers:Int.Set.t;
mutable inductive_status: inductive_status;
- class_type : Term.types;
+ class_type : types;
mutable functions: Int.Set.t PafMap.t} (*pac -> term = app(constr,t) *)
type cl = Rep of representative| Eqto of int*equality