aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/termast.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/termast.ml')
-rw-r--r--parsing/termast.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 95e4b5163..d30e03903 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -18,6 +18,7 @@ open Termops
open Inductive
open Sign
open Environ
+open Libnames
open Declare
open Impargs
open Coqast