aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/cc/ccalgo.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc/ccalgo.ml')
-rw-r--r--plugins/cc/ccalgo.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 4c6156a38..4a691e442 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -130,8 +130,8 @@ type cinfo=
ci_nhyps: int} (* # projectable args *)
let family_eq f1 f2 = match f1, f2 with
- | Prop Pos, Prop Pos
- | Prop Null, Prop Null
+ | Set, Set
+ | Prop, Prop
| Type _, Type _ -> true
| _ -> false