aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/stateid.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-21 20:04:58 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:39:25 +0200
commit02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch)
tree5e55f22c5b20dcf694c00741a69dae6f1d993267 /lib/stateid.ml
parent95239fa33c5da60080833dabc3ced246680dfdf9 (diff)
Remove some unused values and types
Diffstat (limited to 'lib/stateid.ml')
-rw-r--r--lib/stateid.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/lib/stateid.ml b/lib/stateid.ml
index ae25735c5..c153f0e80 100644
--- a/lib/stateid.ml
+++ b/lib/stateid.ml
@@ -32,7 +32,6 @@ let compare = Int.compare
module Self = struct
type t = int
let compare = compare
- let equal = equal
end
module Set = Set.Make(Self)