aboutsummaryrefslogtreecommitdiff
path: root/user-contrib/Ltac2/Ltac2.v
diff options
context:
space:
mode:
Diffstat (limited to 'user-contrib/Ltac2/Ltac2.v')
-rw-r--r--user-contrib/Ltac2/Ltac2.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Ltac2.v b/user-contrib/Ltac2/Ltac2.v
index d3bf3c10ea..ccfc7e4a70 100644
--- a/user-contrib/Ltac2/Ltac2.v
+++ b/user-contrib/Ltac2/Ltac2.v
@@ -22,5 +22,6 @@ Require Ltac2.Fresh.
Require Ltac2.Pattern.
Require Ltac2.Std.
Require Ltac2.Env.
+Require Ltac2.Printf.
Require Ltac2.Ltac1.
Require Export Ltac2.Notations.