aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto')
-rw-r--r--plugins/rtauto/refl_tauto.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 597b6afb6..5a77bf967 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -298,7 +298,7 @@ let rtauto_tac gls=
build_form formula;
build_proof [] 0 prf|]) in
let term=
- Term.applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+ applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
let build_end_time=System.get_time () in
let _ = if !verbose then
begin