diff options
Diffstat (limited to 'translate/ppvernacnew.ml')
| -rw-r--r-- | translate/ppvernacnew.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml index 6bea86fec..985280cfd 100644 --- a/translate/ppvernacnew.ml +++ b/translate/ppvernacnew.ml @@ -94,7 +94,7 @@ let pr_gen env t = (Pptacticnew.pr_raw_tactic env) pr_reference t let pr_raw_tactic tac = - pr_raw_tactic_env [] (Global.env()) tac + Pptacticnew.pr_glob_tactic (Global.env()) (Tacinterp.glob_tactic tac) let rec extract_signature = function | [] -> [] |