Declarative Proof Language: main commit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 1 deletions

diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml
index 801122476..b0e6b6ecf 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;