From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Tue, 21 Nov 2006 21:38:49 +0000 Subject: Imported Upstream version 8.1~gamma --- contrib/rtauto/refl_tauto.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'contrib/rtauto') diff --git a/contrib/rtauto/refl_tauto.ml b/contrib/rtauto/refl_tauto.ml index 445dead2..a1f5e5aa 100644 --- a/contrib/rtauto/refl_tauto.ml +++ b/contrib/rtauto/refl_tauto.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: refl_tauto.ml 7639 2005-12-02 10:01:15Z gregoire $ *) +(* $Id: refl_tauto.ml 9154 2006-09-20 17:18:18Z corbinea $ *) module Search = Explore.Make(Proof_search) @@ -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