diff options
| author | Pierre-Marie Pédrot | 2020-09-28 18:49:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-04 13:43:57 +0100 |
| commit | ae4346d74acf0d3e48a9660758dd7c064d14f749 (patch) | |
| tree | a7960f2855bf6bfd86b9d8fa90c9dcaab32709bf | |
| parent | 5a25287987b8683ee3cbaa9a87ba0f8aebba896b (diff) | |
Further API cleanup after the removal of forward hints.
We know statically that only global references are passed to make_resolves.
| -rw-r--r-- | tactics/class_tactics.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.ml | 5 | ||||
| -rw-r--r-- | tactics/hints.mli | 3 |
3 files changed, 5 insertions, 6 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index ed92a85a12..9e66e8668f 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -482,8 +482,7 @@ let make_resolve_hyp env sigma st only_classes pri decl = let keep = not only_classes || is_class in if keep then let id = GlobRef.VarRef id in - let name = PathHints [id] in - (make_resolves env sigma pri ~name ~check:false (IsGlobRef id)) + make_resolves env sigma pri id else [] let make_hints g (modes,st) only_classes sign = diff --git a/tactics/hints.ml b/tactics/hints.ml index fe3efef7c5..0170487b2e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1365,8 +1365,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun lem -> make_resolves env sigma (eapply, true) empty_hint_info ~check:true lem) lems -let make_resolves env sigma info ~check ?name hint = - make_resolves env sigma (true, false) info ~check ?name hint +let make_resolves env sigma info hint = + let name = PathHints [hint] in + make_resolves env sigma (true, false) info ~check:false ~name (IsGlobRef hint) let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in diff --git a/tactics/hints.mli b/tactics/hints.mli index dd22cff10b..1bbb506761 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -210,8 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> has missing arguments. *) val make_resolves : - env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom -> - hint_term -> hint_entry list + env -> evar_map -> hint_info -> GlobRef.t -> hint_entry list (** [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; |