diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-10-10 17:09:24 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-14 23:29:53 +0100 |
| commit | 0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6 (patch) | |
| tree | d5e2749e9fe2745ad806e86285df9cefe818f63b | |
| parent | 4fd59386e7f60d16bfe9858c372b354d422ac0b6 (diff) | |
[misc] Remove unused binding.
| -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 |