diff options
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/hints.ml | 3 | ||||
| -rw-r--r-- | tactics/hints.mli | 2 |
3 files changed, 6 insertions, 5 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 68a78f52f9..18994d0242 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -524,13 +524,11 @@ let make_resolve_hyp env sigma st only_classes pri decl = (List.map_append (fun (path,info,c) -> let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in - make_resolves env sigma ~name:(PathHints path) - (true, false, false) info ~check:true ~poly:false - h) + make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h) hints) else [] in - (hints @ make_resolves env sigma (true, false, false) pri ~name ~check:false ~poly:false (IsGlobRef id)) + (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id)) else [] let make_hints g (modes,st) only_classes sign = diff --git a/tactics/hints.ml b/tactics/hints.ml index 0c23532e12..58fbf2fd66 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1336,6 +1336,9 @@ let constructor_hints env sigma eapply lems = List.map_append (fun (poly, lem) -> make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems +let make_resolves env sigma info ~check ~poly ?name hint = + make_resolves env sigma (true, false, false) info ~check ~poly ?name hint + let make_local_hint_db env sigma ts eapply lems = let map c = c env sigma in let lems = List.map map lems in diff --git a/tactics/hints.mli b/tactics/hints.mli index 6c8b7fed75..ecbde091cd 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -214,7 +214,7 @@ val prepare_hint : bool (* Check no remaining evars *) -> has missing arguments. *) val make_resolves : - env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> + env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom -> hint_term -> hint_entry list (** [make_resolve_hyp hname htyp]. |