From 0ca1717a3a1243d3fd905bb2f6c3d427f1f98dc6 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 10 Oct 2016 17:09:24 +0200
Subject: [misc] Remove unused binding.

---
 ltac/pptactic.ml | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/ltac/pptactic.ml b/ltac/pptactic.ml
index b1a6fa63d6..fccee6e40a 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
-- 
cgit v1.2.3