diff options
| author | Maxime Dénès | 2019-04-25 12:09:52 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-25 12:09:52 +0200 |
| commit | 392d40134c9cd7dee882e31da96369dd09fbbb45 (patch) | |
| tree | 5f89b9703743038f6940f84b6808e4c84ce39a10 /vendor/Ltac2/_CoqProject | |
| parent | 75c5264aa687480c66a6765d64246b5ebd2c0d54 (diff) | |
| parent | 66b6e83f4f4c32ad86333e13d65329be02c46048 (diff) | |
Merge Ltac2 plugin
Diffstat (limited to 'vendor/Ltac2/_CoqProject')
| -rw-r--r-- | vendor/Ltac2/_CoqProject | 51 |
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 |