aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/tacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacexpr.ml')
-rw-r--r--proofs/tacexpr.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8279b8f9..90dddb748 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -11,6 +11,8 @@ open Topconstr
open Libnames
open Nametab
open Glob_term
+open Errors
+open Pp
open Util
open Genarg
open Pattern