diff options
Diffstat (limited to 'src/ltac2_plugin.mlpack')
| -rw-r--r-- | src/ltac2_plugin.mlpack | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack new file mode 100644 index 0000000000..3d87a8cddb --- /dev/null +++ b/src/ltac2_plugin.mlpack @@ -0,0 +1,7 @@ +Tac2env +Tac2print +Tac2intern +Tac2interp +Tac2entries +Tac2core +G_ltac2 |