aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/rtauto')
-rw-r--r--contrib/rtauto/refl_tauto.ml1
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;