diff options
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 90a8b7fe52..7b8f96cdd8 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -162,6 +162,9 @@ module Hint_db : val cut : t -> hints_path val unfolds : t -> Id.Set.t * Cset.t + + val add_modes : hint_mode array list GlobRef.Map.t -> t -> t + val modes : t -> hint_mode array list GlobRef.Map.t end type hint_db = Hint_db.t |