aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/dad.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/dad.ml')
-rw-r--r--contrib/interface/dad.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index 9d90782e4..3be5d8a36 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -15,6 +15,7 @@ open Ctast;;
open Termast;;
open Astterm;;
open Vernacinterp;;
+open Libnames;;
open Nametab
open Proof_type;;