diff options
| author | Maxime Dénès | 2019-04-25 14:09:42 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-07 10:02:56 +0200 |
| commit | 9779c0bf4945693bfd37b141e2c9f0fea200ba4d (patch) | |
| tree | 26f563e3ad9562bdeb67efe8ff55be5de7fc55e2 /user-contrib/Ltac2/ltac2_plugin.mlpack | |
| parent | 392d40134c9cd7dee882e31da96369dd09fbbb45 (diff) | |
Integrate build and documentation of Ltac2
Since Ltac2 cannot be put under the stdlib logical root (some file names
would clash), we move it to the `user-contrib` directory, to avoid adding
another hardcoded path in `coqinit.ml`, following a suggestion by @ejgallego.
Thanks to @Zimmi48 for the thorough documentation review and the
numerous suggestions.
Diffstat (limited to 'user-contrib/Ltac2/ltac2_plugin.mlpack')
| -rw-r--r-- | user-contrib/Ltac2/ltac2_plugin.mlpack | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/ltac2_plugin.mlpack b/user-contrib/Ltac2/ltac2_plugin.mlpack new file mode 100644 index 0000000000..2a25e825cb --- /dev/null +++ b/user-contrib/Ltac2/ltac2_plugin.mlpack @@ -0,0 +1,14 @@ +Tac2dyn +Tac2ffi +Tac2env +Tac2print +Tac2intern +Tac2interp +Tac2entries +Tac2quote +Tac2match +Tac2core +Tac2extffi +Tac2tactics +Tac2stdlib +G_ltac2 |