aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/coqlib.ml')
-rw-r--r--interp/coqlib.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index d38ef592f..6879dc965 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -15,7 +15,7 @@ open Term
open Libnames
open Pattern
open Nametab
-open Syntax_def
+open Smartlocate
(************************************************************************)
(* Generic functions to find Coq objects *)