diff options
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index c9676ac6f..e5ff47356 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -881,9 +881,9 @@ let pr_goal_selector ~toplevel s = let rec pr_tac inherited tac = let return (doc, l) = (tag tac doc, l) in let (strm, prec) = return (match tac with - | TacAbstract (_,(t,None)) -> + | TacAbstract (t,None) -> keyword "abstract " ++ pr_tac (labstract,L) t, labstract - | TacAbstract (_,(t,Some s)) -> + | TacAbstract (t,Some s) -> hov 0 ( keyword "abstract" ++ str" (" ++ pr_tac (labstract,L) t ++ str")" ++ spc () |