diff options
| -rw-r--r-- | ltac/pptactic.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml index b1a6fa63d..fccee6e40 100644 --- a/ltac/pptactic.ml +++ b/ltac/pptactic.ml @@ -1243,11 +1243,10 @@ let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) (h : 'c extra_genarg_printer) = - let s = match wit with - | ExtraArg s -> ArgT.repr s - | _ -> error - "Can declare a pretty-printing rule only for extra argument types." - in + begin match wit with + | ExtraArg s -> () + | _ -> error "Can declare a pretty-printing rule only for extra argument types." + end; let f x = f pr_constr_expr pr_lconstr_expr pr_raw_tactic_level x in let g x = let env = Global.env () in |