aboutsummaryrefslogtreecommitdiff
path: root/vendor/Ltac2/_CoqProject
diff options
context:
space:
mode:
Diffstat (limited to 'vendor/Ltac2/_CoqProject')
-rw-r--r--vendor/Ltac2/_CoqProject51
1 files changed, 51 insertions, 0 deletions
diff --git a/vendor/Ltac2/_CoqProject b/vendor/Ltac2/_CoqProject
new file mode 100644
index 0000000000..dda5a8001a
--- /dev/null
+++ b/vendor/Ltac2/_CoqProject
@@ -0,0 +1,51 @@
+-R theories/ Ltac2
+-I src/
+
+src/tac2dyn.ml
+src/tac2dyn.mli
+src/tac2expr.mli
+src/tac2types.mli
+src/tac2env.ml
+src/tac2env.mli
+src/tac2print.ml
+src/tac2print.mli
+src/tac2intern.ml
+src/tac2intern.mli
+src/tac2interp.ml
+src/tac2interp.mli
+src/tac2entries.ml
+src/tac2entries.mli
+src/tac2ffi.ml
+src/tac2ffi.mli
+src/tac2qexpr.mli
+src/tac2quote.ml
+src/tac2quote.mli
+src/tac2match.ml
+src/tac2match.mli
+src/tac2core.ml
+src/tac2core.mli
+src/tac2extffi.ml
+src/tac2extffi.mli
+src/tac2tactics.ml
+src/tac2tactics.mli
+src/tac2stdlib.ml
+src/tac2stdlib.mli
+src/g_ltac2.mlg
+src/ltac2_plugin.mlpack
+
+theories/Init.v
+theories/Int.v
+theories/Char.v
+theories/String.v
+theories/Ident.v
+theories/Array.v
+theories/Control.v
+theories/Message.v
+theories/Constr.v
+theories/Pattern.v
+theories/Fresh.v
+theories/Std.v
+theories/Env.v
+theories/Notations.v
+theories/Ltac1.v
+theories/Ltac2.v