From cc7456862743e67d72f0875bc1511070e1658b7a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 6 Jun 2014 19:01:45 +0200
Subject: Dead code.

---
 plugins/decl_mode/decl_proof_instr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 8647ca6769..97989e2687 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -832,7 +832,7 @@ let build_per_info etype casee gls =
   let ctyp=pf_type_of gls casee in
   let is_dep = dependent casee concl in
   let hd,args = decompose_app (special_whd gls ctyp) in
-  let (ind,u as indu) =
+  let (ind,u) =
     try
       destInd hd
     with DestKO ->
-- 
cgit v1.2.3