From 8bc5a5b8fa93a47d9d60a918d9b9b4312e573b08 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 6 Aug 2019 17:03:23 +0200
Subject: [PATCH] [Rmtmps] remove unused type
---
src/kernel_internals/typing/rmtmps.ml | 3 ---
1 file changed, 3 deletions(-)
diff --git a/src/kernel_internals/typing/rmtmps.ml b/src/kernel_internals/typing/rmtmps.ml
index 49684281806..4a6a6f79637 100644
--- a/src/kernel_internals/typing/rmtmps.ml
+++ b/src/kernel_internals/typing/rmtmps.ml
@@ -881,9 +881,6 @@ let removeUnmarked isRoot ast reachable_tbl =
*
*)
-
-type rootsFilter = global -> bool
-
let removeUnused ?(isRoot=isExportedRoot) ast =
if not !keepUnused then
begin
--
GitLab