Factorize code in hint declaration.

This allows to remove internal API from the mli as well.

3 files changed, 10 insertions, 44 deletions

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 80c76bee60..195073d7aa 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -516,25 +516,21 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
   let is_class = iscl env cty in
   let keep = not only_classes || is_class in
     if keep then
-      let c = mkVar id in
-      let name = PathHints [GlobRef.VarRef id] in
+      let id = GlobRef.VarRef id in
+      let name = PathHints [id] in
       let hints =
         if is_class then
-          let hints = build_subclasses ~check:false env sigma (GlobRef.VarRef id) empty_hint_info in
+          let hints = build_subclasses ~check:false env sigma id empty_hint_info in
             (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,not !Flags.quiet) info ~poly:false
+                  (true,false,not !Flags.quiet) info ~check:true ~poly:false
                  h)
                hints)
         else []
       in
-        (hints @ List.map_filter
-         (fun f -> try Some (f (c, cty, Univ.ContextSet.empty))
-           with Failure _ | UserError _ -> None)
-         [make_exact_entry ~name env sigma pri ~poly:false;
-          make_apply_entry ~name env sigma flags pri ~poly:false])
+        (hints @ make_resolves env sigma flags 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 a0670ef70d..0c23532e12 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -882,7 +882,7 @@ let fresh_global_or_constr env sigma poly cr =
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags info ~poly ?name cr =
+let make_resolves env sigma flags info ~check ~poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
@@ -891,7 +891,7 @@ let make_resolves env sigma flags info ~poly ?name cr =
                              [make_exact_entry env sigma info ~poly ?name;
                               make_apply_entry env sigma flags info ~poly ?name]
   in
-  if List.is_empty ents then
+  if check && List.is_empty ents then
     user_err ~hdr:"Hint"
       (pr_leconstr_env env sigma c ++ spc() ++
         (if pi1 flags then str"cannot be used as a hint."
@@ -1183,7 +1183,7 @@ let add_resolves env sigma clist ~local ~superglobal dbnames =
       let r =
         List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
           make_resolves env sigma (true,hnf,not !Flags.quiet)
-            pri ~poly ~name:path gr) clist)
+            pri ~check:true ~poly ~name:path gr) clist)
       in
       let hint = make_hint ~local dbname (AddHints { superglobal; hints = r }) in
       Lib.add_anonymous_leaf (inAutoHint hint))
@@ -1334,7 +1334,7 @@ let expand_constructor_hints env sigma lems =
 let constructor_hints env sigma eapply lems =
   let lems = expand_constructor_hints env sigma lems in
   List.map_append (fun (poly, lem) ->
-      make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems
+      make_resolves env sigma (eapply,true,false) empty_hint_info ~check:true ~poly lem) lems
 
 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 f5fd3348e4..6c8b7fed75 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -206,36 +206,6 @@ val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_
 val prepare_hint : bool (* Check no remaining evars *) ->
   env -> evar_map -> evar_map * constr -> (constr * Univ.ContextSet.t)
 
-(** [make_exact_entry info (c, ctyp, ctx)].
-   [c] is the term given as an exact proof to solve the goal;
-   [ctyp] is the type of [c].
-   [ctx] is its (refreshable) universe context.
-   In info:
-   [hint_priority] is the hint's desired priority, it is 0 if unspecified
-   [hint_pattern] is the hint's desired pattern, it is inferred if not specified
-*)
-
-val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom ->
-  (constr * types * Univ.ContextSet.t) -> hint_entry
-
-(** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
-   [eapply] is true if this hint will be used only with EApply;
-   [hnf] should be true if we should expand the head of cty before searching for
-   products;
-   [c] is the term given as an exact proof to solve the goal;
-   [cty] is the type of [c].
-   [ctx] is its (refreshable) universe context.
-   In info:
-   [hint_priority] is the hint's desired priority, it is computed as the number of products in [cty]
-   if unspecified
-   [hint_pattern] is the hint's desired pattern, it is inferred from the conclusion of [cty]
-   if not specified
-*)
-
-val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
-  (constr * types * Univ.ContextSet.t) -> hint_entry
-
 (** A constr which is Hint'ed will be:
    - (1) used as an Exact, if it does not start with a product
    - (2) used as an Apply, if its HNF starts with a product, and
@@ -244,7 +214,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].