Merge branch 'v8.6'

1 files changed, 25 insertions, 11 deletions

diff --git a/tactics/hints.mli b/tactics/hints.mli
index edc65c407..73cafbefd 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -30,6 +30,8 @@ type debug = Debug | Info | Off
 
 val secvars_of_hyps : Context.Named.t -> Id.Pred.t
 
+val empty_hint_info : 'a hint_info_gen
+
 (** Pre-created hint databases *)
 
 type 'a hint_ast =
@@ -132,20 +134,21 @@ type hint_db = Hint_db.t
 
 type hnf = bool
 
+type hint_info = (patvar list * constr_pattern) hint_info_gen
+
 type hint_term =
   | IsGlobRef of global_reference
   | IsConstr of constr * Univ.universe_context_set
 
 type hints_entry =
-  | HintsResolveEntry of (int option * polymorphic * hnf * hints_path_atom * 
-			  hint_term) list
+  | HintsResolveEntry of
+    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
   | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
-  | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
+  | HintsExternEntry of hint_info * Genarg.glob_generic_argument
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -172,23 +175,34 @@ val prepare_hint : bool (* Check no remaining evars *) ->
   (bool * bool) (* polymorphic or monomorphic, local or global *) ->
   env -> evar_map -> open_constr -> hint_term
 
-(** [make_exact_entry pri (c, ctyp, ctx, secvars)].
+(** [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. *)
-val make_exact_entry : env -> evar_map -> int option -> polymorphic -> ?name:hints_path_atom -> 
+   [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 -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
-(** [make_apply_entry (eapply,hnf,verbose) pri (c,cty,ctx,secvars)].
+(** [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. *)
+   [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 -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   (constr * types * Univ.universe_context_set) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -199,7 +213,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> int option -> polymorphic -> ?name:hints_path_atom -> 
+  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].