diff options
| author | Gaëtan Gilbert | 2020-02-06 17:52:29 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | af788fd0daeed459b98ed9acd3a0443f53666176 (patch) | |
| tree | 678a716ad9776d4acb93c5773d1bedb389949b83 /tactics | |
| parent | ebd1c087298a50f85d3f227452b8a3d1fb7a625c (diff) | |
unsafe_type_of -> type_of in Sequent.extend_with_auto_hints
+ fix evar leak in caller
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 2a9b71387e..9c9f0b7708 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -160,6 +160,8 @@ module Hint_db : val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit + val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a + val use_dn : t -> bool val transparent_state : t -> TransparentState.t val set_transparent_state : t -> TransparentState.t -> t |