diff options
Diffstat (limited to 'parsing/tactic_printer.ml')
| -rw-r--r-- | parsing/tactic_printer.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/tactic_printer.ml b/parsing/tactic_printer.ml index 747d2c738..83dae3dce 100644 --- a/parsing/tactic_printer.ml +++ b/parsing/tactic_printer.ml @@ -16,7 +16,7 @@ open Logic open Printer let pr_tactic = function - | TacArg (Tacexp t) -> + | TacArg (_,Tacexp t) -> (*top tactic from tacinterp*) Pptactic.pr_glob_tactic (Global.env()) t | t -> |