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.ml5
1 files changed, 0 insertions, 5 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index c01214377..898dcd255 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -154,11 +154,6 @@ let rec term_equal t1 t2 =
open Hashset.Combine
-let hash_sorts_family = function
-| InProp -> 0
-| InSet -> 1
-| InType -> 2
-
let rec hash_term = function
| Symb c -> combine 1 (hash_constr c)
| Product (s1, s2) -> combine3 2 (Sorts.hash s1) (Sorts.hash s2)