aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/dischargedhypsmap.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/dischargedhypsmap.ml')
-rw-r--r--library/dischargedhypsmap.ml11
1 files changed, 0 insertions, 11 deletions
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index b8a7da367..c26f652df 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,18 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
-open Util
open Libnames
-open Names
-open Term
-open Reduction
-open Declarations
-open Environ
-open Inductive
-open Libobject
-open Lib
-open Nametab
type discharged_hyps = full_path list