summaryrefslogtreecommitdiff
path: root/parsing/highparsing.mllib
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/highparsing.mllib')
-rw-r--r--parsing/highparsing.mllib7
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/highparsing.mllib b/parsing/highparsing.mllib
new file mode 100644
index 00000000..3eb27abb
--- /dev/null
+++ b/parsing/highparsing.mllib
@@ -0,0 +1,7 @@
+G_constr
+G_vernac
+G_prim
+G_proofs
+G_tactic
+G_ltac
+G_decl_mode