aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/sequent.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/sequent.ml')
-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 6d4d8792f..f0afa2ec5 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -204,7 +204,7 @@ let extend_with_ref_list l seq gl =
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
-open Auto
+open Hints
let extend_with_auto_hints l seq gl=
let seqref=ref seq in