aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccalgo.mli
diff options
context:
space:
mode:
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 f904aa3e6..23cd2161d 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