diff options
| author | ppedrot | 2013-09-03 18:18:32 +0000 |
|---|---|---|
| committer | ppedrot | 2013-09-03 18:18:32 +0000 |
| commit | dd3d3a25ccc58bf06a13dc07db2fc5f88967789c (patch) | |
| tree | cb7605e4d9266d63e68de54d6b9496406e15b79f /tactics/auto.mli | |
| parent | 6338174fdaf790e52062f006c52c911bc5e58cbc (diff) | |
Some cleanup in Auto
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16758 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 5a5b8f56c6..b8860f0978 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Util open Names open Term open Context @@ -117,7 +118,7 @@ val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit val remove_hints : bool -> hint_db_name list -> global_reference list -> unit -val current_db_names : unit -> hint_db_name list +val current_db_names : unit -> String.Set.t val interp_hints : hints_expr -> hints_entry |