diff options
| author | coqbot-app[bot] | 2020-11-16 11:27:08 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 11:27:08 +0000 |
| commit | 57fb6f106f24d2fa1e66a8ac813525f804a7ced7 (patch) | |
| tree | cda92a9bb323790a506ced2759b39684942bdc2a /tactics/hints.mli | |
| parent | 4775fd7724840205b345420507bdd1c7065059b0 (diff) | |
| parent | 7e55f4813d5173d659482a6899c3f97c5346a682 (diff) | |
Merge PR #13388: Export locality for all hint commands
Reviewed-by: silene
Reviewed-by: gares
Reviewed-by: Zimmi48
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 3d4d9c7970..54f4716652 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -189,7 +189,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> TransparentState.t -> bool -> unit -val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit +val remove_hints : locality:Goptions.option_locality -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t |