aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--library/library.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/library/library.ml b/library/library.ml
index cf420d1b7f..5d0a2a5ff2 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -448,7 +448,6 @@ let rec_intern_qualified_library qid =
| LibNotFound ->
errorlabstrm "rec_intern_qualified_library"
(str"Cannot find module " ++ pr_qualid qid ++ str" in loadpath")
- | _ -> assert false
let rec_intern_module_from_file qid f =
(* A name is specified, we have to check it contains module id *)