From 8b1b6e76a6229d9c091bf805e3786bdf0038ae32 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 13 Apr 2017 11:20:20 +0200
Subject: Silence a few OCaml warnings.

---
 plugins/rtauto/refl_tauto.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index f30f8a943..3655df895 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -95,7 +95,6 @@ let rec make_form atom_env gls term =
   let normalize=special_nf gls in
   let cciterm=special_whd gls term  in
   let sigma = Tacmach.project gls in
-  let inj = EConstr.Unsafe.to_constr in
     match EConstr.kind sigma cciterm with
 	Prod(_,a,b) ->
 	  if noccurn sigma 1 b &&
-- 
cgit v1.2.3