aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/rtauto/refl_tauto.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-12 16:20:15 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-12 16:43:33 +0200
commit9097e9a84cf3841cd5fac81a7fe309ae2dec246f (patch)
tree7358a5db6e5f6f17974cc61b4491248f30a332b4 /plugins/rtauto/refl_tauto.ml
parent013c0232953f1f5832c30940119da05847e99ce2 (diff)
parentb6feaafc7602917a8ef86fb8adc9651ff765e710 (diff)
Merge PR#718: API cleanup: aliases
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
-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 b9678fadf..f84eebadc 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -301,7 +301,7 @@ let rtauto_tac gls=
build_form formula;
build_proof [] 0 prf|]) in
let term=
- applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in
+ applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in
let build_end_time=System.get_time () in
let _ = if !verbose then
begin