aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/showproof.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/showproof.ml')
-rw-r--r--contrib/interface/showproof.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index ae876e129..c7e6be131 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -6,6 +6,7 @@ open Environ
open Evd
open Names
open Nameops
+open Libnames
open Term
open Termops
open Util