aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/correctness/pmisc.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/correctness/pmisc.mli')
-rw-r--r--contrib/correctness/pmisc.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index a4359b6d8..3dbae5cd0 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -13,8 +13,6 @@
open Names
open Term
-module SpSet : Set.S with type elt = section_path
-
(* Some misc. functions *)
val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b