aboutsummaryrefslogtreecommitdiff
path: root/vo.itarget
diff options
context:
space:
mode:
Diffstat (limited to 'vo.itarget')
-rw-r--r--vo.itarget7
1 files changed, 7 insertions, 0 deletions
diff --git a/vo.itarget b/vo.itarget
index 776404ad79..5777585681 100644
--- a/vo.itarget
+++ b/vo.itarget
@@ -1 +1,8 @@
+Init.vo
+Int.vo
+String.vo
+Array.vo
+Control.vo
+Message.vo
+Constr.vo
Ltac2.vo