diff options
| author | Pierre-Marie Pédrot | 2020-03-12 15:11:35 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 11:44:50 +0100 |
| commit | 96ec58df041dc0111df0e681269aed9d0e9b571a (patch) | |
| tree | 7abcbb4ec26dfd3fb2ac81934d6e8c8602cc7d80 /tactics | |
| parent | 245b94cd075b6be527590c425a98262d89577909 (diff) | |
Use a 3-valued flag for hint locality.
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 7 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 |
2 files changed, 7 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 8b81b36fa2..7cde342662 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1410,7 +1410,12 @@ let interp_hints ~poly = let _, tacexp = Genintern.generic_intern env tacexp in HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) -let add_hints ~local ~superglobal dbnames h = +let add_hints ~locality dbnames h = + let local, superglobal = match locality with + | Goptions.OptDefault | Goptions.OptGlobal -> false, true + | Goptions.OptExport -> false, false + | Goptions.OptLocal -> true, false + in if String.List.mem "nocore" dbnames then user_err Pp.(str "The hint database \"nocore\" is meant to stay empty."); assert (not (List.is_empty dbnames)); diff --git a/tactics/hints.mli b/tactics/hints.mli index 3fd4d6ea9e..c9d4231d77 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -219,7 +219,7 @@ val current_pure_db : unit -> hint_db list val interp_hints : poly:bool -> hints_expr -> hints_entry -val add_hints : local:bool -> superglobal:bool -> hint_db_name list -> hints_entry -> unit +val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t) |