aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/lemmas.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/lemmas.ml')
-rw-r--r--toplevel/lemmas.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 78aa3fd12..57b623712 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -19,7 +19,7 @@ open Declarations
open Entries
open Environ
open Nameops
-open Libnames
+open Globnames
open Decls
open Decl_kinds
open Declare