From 0f4f723a5608075ff4aa48290314df30843efbcb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Wed, 20 Sep 2006 17:18:18 +0000
Subject: Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/rtauto/refl_tauto.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'contrib/rtauto')

diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index 801122476e..b0e6b6ecff 100644
--- a/contrib/rtauto/refl_tauto.ml
+++ b/contrib/rtauto/refl_tauto.ml
@@ -303,7 +303,6 @@ let rtauto_tac gls=
     end in
   let build_start_time=System.get_time () in
   let _ = step_count := 0; node_count := 0 in
-  let nhyps = List.length hyps in
   let main = mkApp (force node_count l_Reflect,
 		    [|build_env gamma;
 		      build_form formula;
-- 
cgit v1.2.3