aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-11 08:34:50 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-05-11 10:11:57 +0200
commit9a883e3740e21c93c8ea7f51b0cf0c4a76675773 (patch)
tree6f95ae2751b769d889c3c412bd5874dfd2f1f835 /plugins/firstorder
parenteef0ffe1646d09c81de23ad34f58a75d63a88372 (diff)
Rationalizing a bit the interface of Hints.
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 7d034db55..802af04d0 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -209,7 +209,7 @@ open Hints
let extend_with_auto_hints l seq gl=
let seqref=ref seq in
let f p_a_t =
- match repr_auto_tactic p_a_t.code with
+ match repr_hint p_a_t.code with
Res_pf (c,_) | Give_exact (c,_)
| Res_pf_THEN_trivial_fail (c,_) ->
(try