From 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Tue, 7 Oct 2014 17:26:02 +0200
Subject: Splitting out of auto.ml a file hints.ml dedicated to hints so as to
 being able to export hints without tactics, vm, etc. to come with.

Some functions moved to the new proof engine.
---
 plugins/firstorder/sequent.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder/sequent.ml')

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
-- 
cgit v1.2.3