diff options
| author | Pierre-Marie Pédrot | 2017-10-25 12:13:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-10-27 11:48:40 +0200 |
| commit | d4172d2c7a48d932b42248fe57c6c2a87ac57e30 (patch) | |
| tree | 48f49fa0490659f3f505f26ef6fb86d6ae0eae64 /src/ltac2_plugin.mlpack | |
| parent | 0b26bfc8e068e1e95eeea9db0c3bda7436ac8338 (diff) | |
Stubs for goal matching: quotation and matching function.
Diffstat (limited to 'src/ltac2_plugin.mlpack')
| -rw-r--r-- | src/ltac2_plugin.mlpack | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack index a2237f4d26..40b91e4b53 100644 --- a/src/ltac2_plugin.mlpack +++ b/src/ltac2_plugin.mlpack @@ -6,6 +6,7 @@ Tac2intern Tac2interp Tac2entries Tac2quote +Tac2match Tac2core Tac2tactics Tac2stdlib |