aboutsummaryrefslogtreecommitdiff
path: root/vernac/g_proofs.mlg
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/g_proofs.mlg')
-rw-r--r--vernac/g_proofs.mlg1
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 058fa691ee..e84fce5504 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -14,6 +14,7 @@ open Glob_term
open Constrexpr
open Vernacexpr
open Hints
+open ComHints
open Pcoq
open Pcoq.Prim