diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-21 00:15:44 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-27 15:18:11 +0200 |
| commit | b34acd7904dac581b57f7282192a40f1afb870dc (patch) | |
| tree | bf55c06c3571047063abb652b9badd6e1a463cf3 /tactics/hints.mli | |
| parent | 311e87f261b5e7f1dca61ac19d9b7b695b411ce0 (diff) | |
[tactics] Turn boolean locality hint parameter into a named one.
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 c7de10a2a..7ec70e72e 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -178,7 +178,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : polymorphic -> hints_expr -> hints_entry -val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit +val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> (bool * bool) (* polymorphic or monomorphic, local or global *) -> |