aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/sequent.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 571ec4ef34..f75678c60f 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -210,7 +210,7 @@ open Auto
let extend_with_auto_hints l seq gl=
let seqref=ref seq in
- let f (_, p_a_t) =
+ let f p_a_t =
match p_a_t.code with
Res_pf (c,_) | Give_exact c
| Res_pf_THEN_trivial_fail (c,_) ->