diff options
| author | Pierre-Marie Pédrot | 2017-09-07 23:45:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-08 01:36:52 +0200 |
| commit | bdd594093b4fb7e46a6cae0135b6630d75bae6f6 (patch) | |
| tree | 7c59b547c765f61d3de89e6cc71283694089d9d8 /src/ltac2_plugin.mlpack | |
| parent | 643832c053e0255dd356231f4e5887db0228c2cd (diff) | |
Fix coq/ltac2#22: Argument to Tactic_failure should be printed.
We implement a printer for toplevel values and use it for exceptions in
particular.
Diffstat (limited to 'src/ltac2_plugin.mlpack')
| -rw-r--r-- | src/ltac2_plugin.mlpack | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack index 00ba5bc58e..70f97b9d1e 100644 --- a/src/ltac2_plugin.mlpack +++ b/src/ltac2_plugin.mlpack @@ -1,8 +1,8 @@ Tac2dyn Tac2env +Tac2ffi Tac2print Tac2intern -Tac2ffi Tac2interp Tac2entries Tac2quote |