From 6c4eceaa9d71df6cb608b056bebbd760b707d26e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 12:50:26 +0200
Subject: Factorize hint flags in Class_tatcis.make_make_resolve_hyp.

They were always instantiated with the triple (true, false, false).
---
 tactics/class_tactics.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 195073d7aa..72234db688 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -499,7 +499,7 @@ let evars_to_goals p evm =
   else Some (goals, nongoals)
 
 (** Making local hints  *)
-let make_resolve_hyp env sigma st flags only_classes pri decl =
+let make_resolve_hyp env sigma st only_classes pri decl =
   let id = NamedDecl.get_id decl in
   let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in
   let rec iscl env ty =
@@ -530,7 +530,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
                hints)
         else []
       in
-        (hints @ make_resolves env sigma flags pri ~name ~check:false ~poly:false (IsGlobRef id))
+        (hints @ make_resolves env sigma (true, false, false) pri ~name ~check:false ~poly:false (IsGlobRef id))
     else []
 
 let make_hints g (modes,st) only_classes sign =
@@ -546,7 +546,7 @@ let make_hints g (modes,st) only_classes sign =
         in
         if consider then
           let hint =
-            pf_apply make_resolve_hyp g st (true,false,false) only_classes empty_hint_info hyp
+            pf_apply make_resolve_hyp g st only_classes empty_hint_info hyp
           in hint @ hints
         else hints)
       ([]) sign
@@ -793,7 +793,7 @@ module Search = struct
     let decl = Tacmach.New.pf_last_hyp gl in
     let hint =
       make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints)
-                       (true,false,false) info.search_only_classes empty_hint_info decl in
+                       info.search_only_classes empty_hint_info decl in
     let ldb = Hint_db.add_list env sigma hint info.search_hints in
     let info' =
       { info with search_hints = ldb; last_tac = lazy (str"intro");
-- 
cgit v1.2.3


From ca6dd2805b4a00cf8425337ec1d89327c94ef397 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 13:01:36 +0200
Subject: Do not be verbose when declaring subclass hints.

There is no point in warning about eauto being the only one able to use those
hints, since they will be used by typeclass_eauto instead. It was probably an
oversight introduced quite a long time ago.
---
 tactics/class_tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 72234db688..68a78f52f9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -525,7 +525,7 @@ let make_resolve_hyp env sigma st only_classes pri decl =
              (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 ~check:true ~poly:false
+                  (true, false, false) info ~check:true ~poly:false
                  h)
                hints)
         else []
-- 
cgit v1.2.3


From f66bd46c551915267a88d1ee2534ba091292882e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 12:54:27 +0200
Subject: Do not export flags in Hints.make_resolves.

They are always the same.
---
 tactics/class_tactics.ml | 6 ++----
 tactics/hints.ml         | 3 +++
 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].
-- 
cgit v1.2.3


From 7ac18ed989a884e9d44917c916c7aae016582fe4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 14:23:58 +0200
Subject: Do not export Hints.make_extern.

---
 tactics/hints.mli | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/tactics/hints.mli b/tactics/hints.mli
index ecbde091cd..d8881c3b49 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -225,12 +225,6 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-(** [make_extern pri pattern tactic_expr] *)
-
-val make_extern :
-  int -> constr_pattern option -> Genarg.glob_generic_argument
-      -> hint_entry
-
 val run_hint : hint ->
   ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
 
-- 
cgit v1.2.3


From 2a24a665ca63d82ce2576e75636ab6fdbcad9b36 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 15:19:03 +0200
Subject: Remove dead code in the Hints API.

---
 tactics/hints.ml  | 1 -
 tactics/hints.mli | 3 ---
 2 files changed, 4 deletions(-)

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 58fbf2fd66..9595fa2033 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -489,7 +489,6 @@ module Hint_db :
 sig
 type t
 val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
-val find : GlobRef.t -> t -> search_entry
 val map_none : secvars:Id.Pred.t -> t -> full_hint list
 val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
 val map_existential : evar_map -> secvars:Id.Pred.t ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index d8881c3b49..56bd6fad44 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -70,8 +70,6 @@ type 'a with_metadata = private
 
 type full_hint = hint with_metadata
 
-type search_entry
-
 (** The head may not be bound. *)
 
 type hint_entry
@@ -117,7 +115,6 @@ module Hint_db :
   sig
     type t
     val empty : ?name:hint_db_name -> TransparentState.t -> bool -> t
-    val find : GlobRef.t -> t -> search_entry
 
     (** All hints which have no pattern.
      * [secvars] represent the set of section variables that
-- 
cgit v1.2.3


From 21b4e41544f03de18d9f5b1bdb93a26b36a97999 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 15:17:33 +0200
Subject: Opacify the type of hint metadata.

---
 plugins/firstorder/sequent.ml |  2 +-
 tactics/auto.ml               | 12 +++++----
 tactics/class_tactics.ml      | 15 +++++++----
 tactics/eauto.ml              | 13 +++++-----
 tactics/hints.ml              | 15 ++++++++++-
 tactics/hints.mli             | 58 +++++++++++++++++--------------------------
 6 files changed, 62 insertions(+), 53 deletions(-)

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3dd5059e5d..e365151079 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -205,7 +205,7 @@ open Hints
 
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
-    match repr_hint p_a_t.code with
+    match FullHint.repr p_a_t with
     | Res_pf (c,_) | Give_exact (c,_)
     | Res_pf_THEN_trivial_fail (c,_) ->
       let (c, _, _) = c in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 681c4e910f..a73db95884 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -29,7 +29,7 @@ open Hints
 (*          tactics with a trace mechanism for automatic search           *)
 (**************************************************************************)
 
-let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l
+let priority l = List.filter (fun (_, hint) -> Int.equal (FullHint.priority hint) 0) l
 
 let compute_secvars gl =
   let hyps = Proofview.Goal.hyps gl in
@@ -381,7 +381,8 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
           in List.map (fun x -> (Some flags,x)) l)
         (local_db::db_list)
 
-and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
+and tac_of_hint dbg db_list local_db concl (flags, h) =
+  let poly = FullHint.is_polymorphic h in
   let tactic = function
     | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
@@ -403,16 +404,17 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
          Tacticals.New.tclFAIL ~info 0 (str"Unbound reference")
        end
     | Extern tacast ->
+      let p = FullHint.pattern h in
       conclPattern concl p tacast
   in
   let pr_hint env sigma =
-    let origin = match dbname with
+    let origin = match FullHint.database h with
     | None -> mt ()
     | Some n -> str " (in " ++ str n ++ str ")"
     in
-    pr_hint env sigma t ++ origin
+    FullHint.print env sigma h ++ origin
   in
-  tclLOG dbg pr_hint (run_hint t tactic)
+  tclLOG dbg pr_hint (FullHint.run h tactic)
 
 and trivial_resolve sigma dbg mod_delta db_list local_db secvars cl =
   try
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 18994d0242..2c9d06f5b9 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -346,7 +346,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
     with e when CErrors.noncritical e -> AllowAll
   in
   let tac_of_hint =
-    fun (flags, {pri = b; pat = p; poly = poly; code = t; secvars; name = name}) ->
+    fun (flags, h) ->
+      let b = FullHint.priority h in
+      let poly = FullHint.is_polymorphic h in
+      let p = FullHint.pattern h in
+      let secvars = FullHint.secvars h in (* The use below looks suspicious *)
+      let name = FullHint.name h in
       let tac = function
         | Res_pf (term,cl) ->
            if get_typeclasses_filtered_unification () then
@@ -391,7 +396,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
          Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c])
       | Extern tacast -> conclPattern concl p tacast
       in
-      let tac = run_hint t tac in
+      let tac = FullHint.run h tac in
       let tac = if complete then Tacticals.New.tclCOMPLETE tac else tac in
       let pp =
         match p with
@@ -399,9 +404,9 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
            str " with pattern " ++ Printer.pr_constr_pattern_env env sigma pat
         | _ -> mt ()
       in
-        match repr_hint t with
-        | Extern _ -> (tac, b, true, name, lazy (pr_hint env sigma t ++ pp))
-        | _ -> (tac, b, false, name, lazy (pr_hint env sigma t ++ pp))
+        match FullHint.repr h with
+        | Extern _ -> (tac, b, true, name, lazy (FullHint.print env sigma h ++ pp))
+        | _ -> (tac, b, false, name, lazy (FullHint.print env sigma h ++ pp))
   in
   let hint_of_db = hintmap_of sigma hdc secvars concl in
   let hintl = List.map_filter (fun db -> match hint_of_db db with
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index c2eabffd44..7a141bb53b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -120,10 +120,11 @@ and e_my_find_search env sigma db_list local_db secvars concl =
           List.map (fun x -> flags, x) (hint_of_db db)) (local_db::db_list)
   in
   let tac_of_hint =
-    fun (st, {pri = b; pat = p; code = t; poly = poly}) ->
-      let b = match Hints.repr_hint t with
+    fun (st, h) ->
+      let poly = FullHint.is_polymorphic h in
+      let b = match FullHint.repr h with
       | Unfold_nth _ -> 1
-      | _ -> b
+      | _ -> FullHint.priority h
       in
       let tac = function
       | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
@@ -133,10 +134,10 @@ and e_my_find_search env sigma db_list local_db secvars concl =
         Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
-      | Extern tacast -> conclPattern concl p tacast
+      | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
       in
-      let tac = run_hint t tac in
-      (tac, b, lazy (pr_hint env sigma t))
+      let tac = FullHint.run h tac in
+      (tac, b, lazy (FullHint.print env sigma h))
   in
   List.map tac_of_hint hintl
 
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9595fa2033..78ed81ec37 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1576,4 +1576,17 @@ let run_hint tac k = match warn_hint () with
     let info = Exninfo.reify () in
     Proofview.tclZERO ~info (UserError (None, (str "Tactic failure.")))
 
-let repr_hint h = h.obj
+module FullHint =
+struct
+  type t = full_hint
+  let priority (h : t) = h.pri
+  let is_polymorphic (h : t) = h.poly
+  let pattern (h : t) = h.pat
+  let database (h : t) = h.db
+  let run (h : t) k = run_hint h.code k
+  let print env sigma (h : t) = pr_hint env sigma h.code
+  let name (h : t) = h.name
+  let secvars (h : t) = h.secvars
+
+  let repr (h : t) = h.code.obj
+end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 56bd6fad44..4e7abad2b6 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -15,7 +15,6 @@ open Environ
 open Evd
 open Tactypes
 open Clenv
-open Pattern
 open Typeclasses
 
 (** {6 General functions. } *)
@@ -40,7 +39,6 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
-type hint
 type raw_hint = constr * types * Univ.ContextSet.t
 
 type 'a hints_path_atom_gen =
@@ -51,24 +49,22 @@ type 'a hints_path_atom_gen =
 type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
-type 'a with_metadata = private
-  { pri     : int
-  (** A number lower is higher priority *)
-  ; poly    : bool
-  (** Is the hint polymorpic and hence should be refreshed at each application *)
-  ; pat     : constr_pattern option
-  (** A pattern for the concl of the Goal *)
-  ; name    : hints_path_atom
-  (** A potential name to refer to the hint *)
-  ; db : string option
-  (** The database from which the hint comes *)
-  ; secvars : Id.Pred.t
-  (** The set of section variables the hint depends on *)
-  ; code    : 'a
-  (** the tactic to apply when the concl matches pat *)
-  }
-
-type full_hint = hint with_metadata
+module FullHint :
+sig
+  type t
+  val priority : t -> int
+  val is_polymorphic : t -> bool
+  val pattern : t -> Pattern.constr_pattern option
+  val database : t -> string option
+  val run : t -> ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  val name : t -> hints_path_atom
+  val secvars : t -> Id.Pred.t
+  val print : env -> evar_map -> t -> Pp.t
+
+  (** This function is for backward compatibility only, not to use in newly
+    written code. *)
+  val repr : t -> (raw_hint * clausenv) hint_ast
+end
 
 (** The head may not be bound. *)
 
@@ -119,37 +115,37 @@ module Hint_db :
     (** All hints which have no pattern.
      * [secvars] represent the set of section variables that
      * can be used in the hint. *)
-    val map_none : secvars:Id.Pred.t -> t -> full_hint list
+    val map_none : secvars:Id.Pred.t -> t -> FullHint.t list
 
     (** All hints associated to the reference *)
-    val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list
+    val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> FullHint.t list
 
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments, _not_ using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches.
         *)
     val map_existential : evar_map -> secvars:Id.Pred.t ->
-      (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
+      (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference, respecting modes if evars appear in the
         arguments and using the discrimination net.
         Returns a [ModeMismatch] if there are declared modes and none matches. *)
-    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list with_mode
+    val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> FullHint.t list with_mode
 
     (** All hints associated to the reference.
         Precondition: no evars should appear in the arguments, so no modes
         are checked. *)
     val map_auto : evar_map -> secvars:Id.Pred.t ->
-       (GlobRef.t * constr array) -> constr -> t -> full_hint list
+       (GlobRef.t * constr array) -> constr -> t -> FullHint.t list
 
     val add_one : env -> evar_map -> hint_entry -> t -> t
     val add_list : env -> evar_map -> hint_entry list -> t -> t
     val remove_one : GlobRef.t -> t -> t
     val remove_list : GlobRef.t list -> t -> t
     val iter : (GlobRef.t option ->
-                hint_mode array list -> full_hint list -> unit) -> t -> unit
+                hint_mode array list -> FullHint.t list -> unit) -> t -> unit
 
-    val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a
+    val fold : (GlobRef.t option -> hint_mode array list -> FullHint.t list -> 'a -> 'a) -> t -> 'a -> 'a
 
     val use_dn : t -> bool
     val transparent_state : t -> TransparentState.t
@@ -222,13 +218,6 @@ val make_resolves :
 val make_resolve_hyp :
   env -> evar_map -> named_declaration -> hint_entry list
 
-val run_hint : hint ->
-  ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
-
-(** This function is for backward compatibility only, not to use in newly
-    written code. *)
-val repr_hint : hint -> (raw_hint * clausenv) hint_ast
-
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)
@@ -253,4 +242,3 @@ val pr_applicable_hint : Proof.t -> Pp.t
 val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t
 val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t
 val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t
-val pr_hint : env -> evar_map -> hint -> Pp.t
-- 
cgit v1.2.3


From 437f86aaa55bbae99742b600bb52a234d75667e5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 16:21:21 +0200
Subject: Remove access to hint section variables.

The only use was seemingly a bug introduced in 0aec9033a by an accidental
variable capture. There is indeed no reason that the set of variables of a
hint corresponds to the one of the current environment.
---
 tactics/class_tactics.ml | 1 -
 tactics/hints.ml         | 1 -
 tactics/hints.mli        | 1 -
 3 files changed, 3 deletions(-)

diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 2c9d06f5b9..b435d560c7 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -350,7 +350,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
       let b = FullHint.priority h in
       let poly = FullHint.is_polymorphic h in
       let p = FullHint.pattern h in
-      let secvars = FullHint.secvars h in (* The use below looks suspicious *)
       let name = FullHint.name h in
       let tac = function
         | Res_pf (term,cl) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 78ed81ec37..63ca4b8834 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1586,7 +1586,6 @@ struct
   let run (h : t) k = run_hint h.code k
   let print env sigma (h : t) = pr_hint env sigma h.code
   let name (h : t) = h.name
-  let secvars (h : t) = h.secvars
 
   let repr (h : t) = h.code.obj
 end
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 4e7abad2b6..01b373b284 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -58,7 +58,6 @@ sig
   val database : t -> string option
   val run : t -> ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
   val name : t -> hints_path_atom
-  val secvars : t -> Id.Pred.t
   val print : env -> evar_map -> t -> Pp.t
 
   (** This function is for backward compatibility only, not to use in newly
-- 
cgit v1.2.3


From 9eca7cca68dc82aa738a8d408d75e1b9b5405646 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 18:57:25 +0200
Subject: Wrap the content of full hints into a record.

---
 plugins/firstorder/sequent.ml |  6 ++---
 tactics/auto.ml               | 19 +++++++--------
 tactics/auto.mli              |  4 ++--
 tactics/class_tactics.ml      | 54 +++++++++++++++++++++++--------------------
 tactics/eauto.ml              | 18 +++++++--------
 tactics/hints.ml              | 31 +++++++++++++++----------
 tactics/hints.mli             | 11 ++++++---
 7 files changed, 80 insertions(+), 63 deletions(-)

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index e365151079..db3631daa4 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -206,9 +206,9 @@ open Hints
 let extend_with_auto_hints env sigma l seq =
   let f (seq,sigma) p_a_t =
     match FullHint.repr p_a_t with
-    | Res_pf (c,_) | Give_exact (c,_)
-    | Res_pf_THEN_trivial_fail (c,_) ->
-      let (c, _, _) = c in
+    | Res_pf c | Give_exact c
+    | Res_pf_THEN_trivial_fail c ->
+      let c = c.hint_term in
       (match  EConstr.destRef sigma c with
        | exception Constr.DestKO -> seq, sigma
        | gr, _ ->
diff --git a/tactics/auto.ml b/tactics/auto.ml
index a73db95884..4ed01d4e65 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,8 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
+let connect_hint_clenv ~poly h gl =
+  let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
      below just replaces the metas of sigma by those coming from the clenv. *)
@@ -95,9 +96,9 @@ let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve ~poly flags ((c : raw_hint), clenv) =
+let unify_resolve ~poly flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv ~poly c clenv gl in
+  let clenv, c = connect_hint_clenv ~poly h gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
@@ -108,9 +109,9 @@ let unify_resolve_gen ~poly = function
   | None -> unify_resolve_nodelta poly
   | Some flags -> unify_resolve ~poly flags
 
-let exact poly (c,clenv) =
+let exact poly h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -384,14 +385,14 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 and tac_of_hint dbg db_list local_db concl (flags, h) =
   let poly = FullHint.is_polymorphic h in
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
+    | Res_pf h -> unify_resolve_gen ~poly flags h
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
         let info = Exninfo.reify () in
         Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
-    | Give_exact (c, cl)  -> exact poly (c, cl)
-    | Res_pf_THEN_trivial_fail (c,cl) ->
+    | Give_exact h  -> exact poly h
+    | Res_pf_THEN_trivial_fail h ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen ~poly flags (c,cl))
+        (unify_resolve_gen ~poly flags h)
         (* With "(debug) trivial", we shouldn't end here, and
            with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 33deefd0bd..9be58cb3fa 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ val default_search_depth : int ref
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
 val connect_hint_clenv
-  : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr
+  : poly:bool -> hint -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
+val unify_resolve : poly:bool -> Unification.unify_flags -> hint -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b435d560c7..fe7b62b316 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,11 +144,11 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly (c,clenv) =
+let e_give_exact flags poly h =
+  let { hint_term = c; hint_clnv = clenv } = h in
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
-  let (c, _, _) = c in
   let c, sigma =
     if poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
@@ -173,17 +173,18 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
 
-let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', c = connect_hint_clenv ~poly c clenv gls in
+let unify_e_resolve poly flags = begin fun gls (h, _) ->
+  let clenv', c = connect_hint_clenv ~poly h gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
-let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', _ = connect_hint_clenv ~poly c clenv gls in
+let unify_resolve poly flags = begin fun gls (h, _) ->
+  let clenv', _ = connect_hint_clenv ~poly h gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) =
+let unify_resolve_refine poly flags gls (h, n) =
+  let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
@@ -221,8 +222,8 @@ let unify_resolve_refine poly flags gl clenv =
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
 *)
-let clenv_of_prods poly nprods (c, clenv) gl =
-  let (c, _, _) = c in
+let clenv_of_prods poly nprods h gl =
+  let { hint_term = c; hint_clnv = clenv } = h in
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
     let sigma = Tacmach.New.project gl in
@@ -234,20 +235,22 @@ let clenv_of_prods poly nprods (c, clenv) gl =
             mk_clenv_from_n gl (Some diff) (c,ty))
     else None
 
-let with_prods nprods poly (c, clenv) f =
+let with_prods nprods poly h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      try match clenv_of_prods poly nprods (c, clenv) gl with
+      try match clenv_of_prods poly nprods h gl with
           | None ->
             let info = Exninfo.reify () in
             Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
-          | Some (diff, clenv') -> f gl (c, diff, clenv')
+          | Some (diff, clenv') ->
+            let h = { h with hint_clnv = clenv' } in
+            f gl (h, diff)
       with e when CErrors.noncritical e ->
         let e, info = Exninfo.capture e in
         Tacticals.New.tclZEROMSG ~info (CErrors.print e) end
   else Proofview.Goal.enter
          begin fun gl ->
-         if Int.equal nprods 0 then f gl (c, None, clenv)
+         if Int.equal nprods 0 then f gl (h, None)
          else Tacticals.New.tclZEROMSG (str"Not enough premisses") end
 
 let matches_pattern concl pat =
@@ -352,42 +355,42 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
       let p = FullHint.pattern h in
       let name = FullHint.name h in
       let tac = function
-        | Res_pf (term,cl) ->
+        | Res_pf h ->
            if get_typeclasses_filtered_unification () then
              let tac =
-               with_prods nprods poly (term,cl)
+               with_prods nprods poly h
                           (fun gl clenv ->
                              matches_pattern concl p <*>
                                unify_resolve_refine poly flags gl clenv)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly (term,cl) (unify_resolve poly flags) in
+               with_prods nprods poly h (unify_resolve poly flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-        | ERes_pf (term,cl) ->
+        | ERes_pf h ->
            if get_typeclasses_filtered_unification () then
-             let tac = (with_prods nprods poly (term,cl)
+             let tac = (with_prods nprods poly h
                   (fun gl clenv ->
                              matches_pattern concl p <*>
                              unify_resolve_refine poly flags gl clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
+               with_prods nprods poly h (unify_e_resolve poly flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
-        | Give_exact (c,clenv) ->
+        | Give_exact h ->
            if get_typeclasses_filtered_unification () then
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.enter
-                   (fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
+                   (fun gl -> unify_resolve_refine poly flags gl (h, None)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             e_give_exact flags poly (c,clenv)
-      | Res_pf_THEN_trivial_fail (term,cl) ->
-         let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
+             e_give_exact flags poly h
+      | Res_pf_THEN_trivial_fail h ->
+         let fst = with_prods nprods poly h (unify_e_resolve poly flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
@@ -1248,7 +1251,8 @@ let autoapply c i =
     (Hints.Hint_db.transparent_state hintdb) in
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-    unify_e_resolve false flags gl ((c,cty,Univ.ContextSet.empty),0,ce) <*>
+  let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce } in
+    unify_e_resolve false flags gl (h, 0) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 7a141bb53b..4a6364795b 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -65,9 +65,9 @@ open Auto
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let unify_e_resolve poly flags (c,clenv) =
+let unify_e_resolve poly flags h =
   Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv ~poly c clenv gl in
+      let clenv', c = connect_hint_clenv ~poly h gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl =
      else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
-let e_exact poly flags (c,clenv) =
+let e_exact poly flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -127,11 +127,11 @@ and e_my_find_search env sigma db_list local_db secvars concl =
       | _ -> FullHint.priority h
       in
       let tac = function
-      | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
-      | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
-      | Give_exact (c,cl) -> e_exact poly st (c,cl)
-      | Res_pf_THEN_trivial_fail (term,cl) ->
-        Tacticals.New.tclTHEN (unify_e_resolve poly st (term,cl))
+      | Res_pf h -> unify_resolve ~poly st h
+      | ERes_pf h -> unify_e_resolve poly st h
+      | Give_exact h -> e_exact poly st h
+      | Res_pf_THEN_trivial_fail h ->
+        Tacticals.New.tclTHEN (unify_e_resolve poly st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
       | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 63ca4b8834..0a213d5d0e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -137,7 +137,12 @@ type 'a with_uid = {
 
 type raw_hint = constr * types * Univ.ContextSet.t
 
-type hint = (raw_hint * clausenv) hint_ast with_uid
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+}
 
 type 'a with_metadata =
   { pri     : int
@@ -156,7 +161,7 @@ type 'a with_metadata =
   (** the tactic to apply when the concl matches pat *)
   }
 
-type full_hint = hint with_metadata
+type full_hint = hint hint_ast with_uid with_metadata
 
 type hint_entry = GlobRef.t option *
   raw_hint hint_ast with_uid with_metadata
@@ -303,16 +308,18 @@ let instantiate_hint env sigma p =
   let mk_clenv (c, cty, ctx) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
-      {cl with templval =
+    let cl = {cl with templval =
           { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
         env = empty_env}
+    in
+    { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
   in
   let code = match p.code.obj with
-    | Res_pf c -> Res_pf (c, mk_clenv c)
-    | ERes_pf c -> ERes_pf (c, mk_clenv c)
+    | Res_pf c -> Res_pf (mk_clenv c)
+    | ERes_pf c -> ERes_pf (mk_clenv c)
     | Res_pf_THEN_trivial_fail c ->
-      Res_pf_THEN_trivial_fail (c, mk_clenv c)
-    | Give_exact c -> Give_exact (c, mk_clenv c)
+      Res_pf_THEN_trivial_fail (mk_clenv c)
+    | Give_exact c -> Give_exact (mk_clenv c)
     | Unfold_nth e -> Unfold_nth e
     | Extern t -> Extern t
   in
@@ -1367,13 +1374,13 @@ let make_db_list dbnames =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let pr_hint_elt env sigma (c, _, _) = pr_econstr_env env sigma c
+let pr_hint_elt env sigma h = pr_econstr_env env sigma h.hint_term
 
 let pr_hint env sigma h = match h.obj with
-  | Res_pf (c, _) -> (str"simple apply " ++ pr_hint_elt env sigma c)
-  | ERes_pf (c, _) -> (str"simple eapply " ++ pr_hint_elt env sigma c)
-  | Give_exact (c, _) -> (str"exact " ++ pr_hint_elt env sigma c)
-  | Res_pf_THEN_trivial_fail (c, _) ->
+  | Res_pf c -> (str"simple apply " ++ pr_hint_elt env sigma c)
+  | ERes_pf c -> (str"simple eapply " ++ pr_hint_elt env sigma c)
+  | Give_exact c -> (str"exact " ++ pr_hint_elt env sigma c)
+  | Res_pf_THEN_trivial_fail c ->
       (str"simple apply " ++ pr_hint_elt env sigma c ++ str" ; trivial")
   | Unfold_nth c ->
     str"unfold " ++  pr_evaluable_reference c
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 01b373b284..29fd90d3ef 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -39,7 +39,12 @@ type 'a hint_ast =
   | Unfold_nth of evaluable_global_reference       (* Hint Unfold *)
   | Extern     of Genarg.glob_generic_argument       (* Hint Extern *)
 
-type raw_hint = constr * types * Univ.ContextSet.t
+type hint = {
+  hint_term : constr;
+  hint_type : types;
+  hint_uctx : Univ.ContextSet.t;
+  hint_clnv : clausenv;
+}
 
 type 'a hints_path_atom_gen =
   | PathHints of 'a list
@@ -56,13 +61,13 @@ sig
   val is_polymorphic : t -> bool
   val pattern : t -> Pattern.constr_pattern option
   val database : t -> string option
-  val run : t -> ((raw_hint * clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
+  val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
   val name : t -> hints_path_atom
   val print : env -> evar_map -> t -> Pp.t
 
   (** This function is for backward compatibility only, not to use in newly
     written code. *)
-  val repr : t -> (raw_hint * clausenv) hint_ast
+  val repr : t -> hint hint_ast
 end
 
 (** The head may not be bound. *)
-- 
cgit v1.2.3


From c00a369a8bd70efad3e1481daa78ab483038c6cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 8 Jun 2020 19:20:02 +0200
Subject: Move the hint polymorphic status to the hint instance.

It is only used for this kind of hints, never for Extern / Unfold.
---
 tactics/auto.ml          | 27 ++++++++++-----------
 tactics/auto.mli         |  4 +--
 tactics/class_tactics.ml | 51 +++++++++++++++++++--------------------
 tactics/eauto.ml         | 17 ++++++-------
 tactics/hints.ml         | 63 +++++++++++++++++++++++-------------------------
 tactics/hints.mli        |  2 +-
 6 files changed, 79 insertions(+), 85 deletions(-)

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4ed01d4e65..f041af1db1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv ~poly h gl =
+let connect_hint_clenv h gl =
   let { hint_term = c; hint_uctx = ctx; hint_clnv = clenv } = h in
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
@@ -78,7 +78,7 @@ let connect_hint_clenv ~poly h gl =
   let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
   (* Still, we need to update the universes *)
   let clenv, c =
-    if poly then
+    if h.hint_poly then
       (* Refresh the instance of the hint *)
       let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
       let emap c = Vars.subst_univs_level_constr subst c in
@@ -96,22 +96,22 @@ let connect_hint_clenv ~poly h gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve ~poly flags (h : hint) =
+let unify_resolve flags (h : hint) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv ~poly h gl in
+  let clenv, c = connect_hint_clenv h gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
 
-let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
+let unify_resolve_nodelta h = unify_resolve auto_unif_flags h
 
-let unify_resolve_gen ~poly = function
-  | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve ~poly flags
+let unify_resolve_gen = function
+  | None -> unify_resolve_nodelta
+  | Some flags -> unify_resolve flags
 
-let exact poly h =
+let exact h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly h gl in
+    let clenv', c = connect_hint_clenv h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -383,16 +383,15 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
         (local_db::db_list)
 
 and tac_of_hint dbg db_list local_db concl (flags, h) =
-  let poly = FullHint.is_polymorphic h in
   let tactic = function
-    | Res_pf h -> unify_resolve_gen ~poly flags h
+    | Res_pf h -> unify_resolve_gen flags h
     | ERes_pf _ -> Proofview.Goal.enter (fun gl ->
         let info = Exninfo.reify () in
         Tacticals.New.tclZEROMSG ~info (str "eres_pf"))
-    | Give_exact h  -> exact poly h
+    | Give_exact h  -> exact h
     | Res_pf_THEN_trivial_fail h ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen ~poly flags h)
+        (unify_resolve_gen flags h)
         (* With "(debug) trivial", we shouldn't end here, and
            with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 9be58cb3fa..903da143d2 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -24,10 +24,10 @@ val default_search_depth : int ref
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
 val connect_hint_clenv
-  : poly:bool -> hint -> Proofview.Goal.t -> clausenv * constr
+  : hint -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : poly:bool -> Unification.unify_flags -> hint -> unit Proofview.tactic
+val unify_resolve : Unification.unify_flags -> hint -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index fe7b62b316..484aab2f00 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -144,13 +144,13 @@ let auto_unif_flags ?(allowed_evars = AllowAll) st =
     resolve_evars = false
 }
 
-let e_give_exact flags poly h =
+let e_give_exact flags h =
   let { hint_term = c; hint_clnv = clenv } = h in
   let open Tacmach.New in
   Proofview.Goal.enter begin fun gl ->
   let sigma = project gl in
   let c, sigma =
-    if poly then
+    if h.hint_poly then
       let clenv', subst = Clenv.refresh_undefined_univs clenv in
       let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
       let c = Vars.subst_univs_level_constr subst c in
@@ -173,24 +173,24 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
        Clenvtac.clenv_refine ~with_evars ~with_classes:false clenv'
   end
 
-let unify_e_resolve poly flags = begin fun gls (h, _) ->
-  let clenv', c = connect_hint_clenv ~poly h gls in
+let unify_e_resolve flags = begin fun gls (h, _) ->
+  let clenv', c = connect_hint_clenv h gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
-let unify_resolve poly flags = begin fun gls (h, _) ->
-  let clenv', _ = connect_hint_clenv ~poly h gls in
+let unify_resolve flags = begin fun gls (h, _) ->
+  let clenv', _ = connect_hint_clenv h gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
 (** Application of a lemma using [refine] instead of the old [w_unify] *)
-let unify_resolve_refine poly flags gls (h, n) =
+let unify_resolve_refine flags gls (h, n) =
   let { hint_term = c; hint_type = t; hint_uctx = ctx; hint_clnv = clenv } = h in
   let open Clenv in
   let env = Proofview.Goal.env gls in
   let concl = Proofview.Goal.concl gls in
   Refine.refine ~typecheck:false begin fun sigma ->
       let sigma, term, ty =
-        if poly then
+        if h.hint_poly then
           let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
           let map c = Vars.subst_univs_level_constr subst c in
           let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
@@ -207,9 +207,9 @@ let unify_resolve_refine poly flags gls (h, n) =
                               env sigma' cl.cl_concl concl)
       in (sigma', term) end
 
-let unify_resolve_refine poly flags gl clenv =
+let unify_resolve_refine flags gl clenv =
   Proofview.tclORELSE
-    (unify_resolve_refine poly flags gl clenv)
+    (unify_resolve_refine flags gl clenv)
     (fun (exn,info) ->
       match exn with
       | Evarconv.UnableToUnify _ ->
@@ -222,8 +222,8 @@ let unify_resolve_refine poly flags gl clenv =
 (** Dealing with goals of the form A -> B and hints of the form
   C -> A -> B.
 *)
-let clenv_of_prods poly nprods h gl =
-  let { hint_term = c; hint_clnv = clenv } = h in
+let clenv_of_prods nprods h gl =
+  let { hint_term = c; hint_clnv = clenv; hint_poly = poly } = h in
   if poly || Int.equal nprods 0 then Some (None, clenv)
   else
     let sigma = Tacmach.New.project gl in
@@ -235,10 +235,10 @@ let clenv_of_prods poly nprods h gl =
             mk_clenv_from_n gl (Some diff) (c,ty))
     else None
 
-let with_prods nprods poly h f =
+let with_prods nprods h f =
   if get_typeclasses_limit_intros () then
     Proofview.Goal.enter begin fun gl ->
-      try match clenv_of_prods poly nprods h gl with
+      try match clenv_of_prods nprods h gl with
           | None ->
             let info = Exninfo.reify () in
             Tacticals.New.tclZEROMSG ~info (str"Not enough premisses")
@@ -351,33 +351,32 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
   let tac_of_hint =
     fun (flags, h) ->
       let b = FullHint.priority h in
-      let poly = FullHint.is_polymorphic h in
       let p = FullHint.pattern h in
       let name = FullHint.name h in
       let tac = function
         | Res_pf h ->
            if get_typeclasses_filtered_unification () then
              let tac =
-               with_prods nprods poly h
+               with_prods nprods h
                           (fun gl clenv ->
                              matches_pattern concl p <*>
-                               unify_resolve_refine poly flags gl clenv)
+                               unify_resolve_refine flags gl clenv)
              in Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly h (unify_resolve poly flags) in
+               with_prods nprods h (unify_resolve flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
         | ERes_pf h ->
            if get_typeclasses_filtered_unification () then
-             let tac = (with_prods nprods poly h
+             let tac = (with_prods nprods h
                   (fun gl clenv ->
                              matches_pattern concl p <*>
-                             unify_resolve_refine poly flags gl clenv)) in
+                             unify_resolve_refine flags gl clenv)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
              let tac =
-               with_prods nprods poly h (unify_e_resolve poly flags) in
+               with_prods nprods h (unify_e_resolve flags) in
                Proofview.tclBIND (Proofview.with_shelf tac)
                   (fun (gls, ()) -> shelve_dependencies gls)
         | Give_exact h ->
@@ -385,12 +384,12 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
              let tac =
                matches_pattern concl p <*>
                  Proofview.Goal.enter
-                   (fun gl -> unify_resolve_refine poly flags gl (h, None)) in
+                   (fun gl -> unify_resolve_refine flags gl (h, None)) in
              Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
            else
-             e_give_exact flags poly h
+             e_give_exact flags h
       | Res_pf_THEN_trivial_fail h ->
-         let fst = with_prods nprods poly h (unify_e_resolve poly flags) in
+         let fst = with_prods nprods h (unify_e_resolve flags) in
          let snd = if complete then Tacticals.New.tclIDTAC
                    else e_trivial_fail_db only_classes db_list local_db secvars in
          Tacticals.New.tclTHEN fst snd
@@ -1251,8 +1250,8 @@ let autoapply c i =
     (Hints.Hint_db.transparent_state hintdb) in
   let cty = Tacmach.New.pf_get_type_of gl c in
   let ce = mk_clenv_from gl (c,cty) in
-  let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce } in
-    unify_e_resolve false flags gl (h, 0) <*>
+  let h = { hint_term = c; hint_type = cty; hint_uctx = Univ.ContextSet.empty; hint_clnv = ce; hint_poly = false } in
+    unify_e_resolve flags gl (h, 0) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
       let sigma = Typeclasses.make_unresolvables
           (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 4a6364795b..0ff90bc046 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -65,9 +65,9 @@ open Auto
 (* A tactic similar to Auto, but using EApply, Assumption and e_give_exact *)
 (***************************************************************************)
 
-let unify_e_resolve poly flags h =
+let unify_e_resolve flags h =
   Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv ~poly h gl in
+      let clenv', c = connect_hint_clenv h gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -88,9 +88,9 @@ let hintmap_of sigma secvars concl =
      else (fun db -> Hint_db.map_auto sigma ~secvars hdc concl db)
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
-let e_exact poly flags h =
+let e_exact flags h =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv ~poly h gl in
+    let clenv', c = connect_hint_clenv h gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -121,17 +121,16 @@ and e_my_find_search env sigma db_list local_db secvars concl =
   in
   let tac_of_hint =
     fun (st, h) ->
-      let poly = FullHint.is_polymorphic h in
       let b = match FullHint.repr h with
       | Unfold_nth _ -> 1
       | _ -> FullHint.priority h
       in
       let tac = function
-      | Res_pf h -> unify_resolve ~poly st h
-      | ERes_pf h -> unify_e_resolve poly st h
-      | Give_exact h -> e_exact poly st h
+      | Res_pf h -> unify_resolve st h
+      | ERes_pf h -> unify_e_resolve st h
+      | Give_exact h -> e_exact st h
       | Res_pf_THEN_trivial_fail h ->
-        Tacticals.New.tclTHEN (unify_e_resolve poly st h)
+        Tacticals.New.tclTHEN (unify_e_resolve st h)
           (e_trivial_fail_db db_list local_db)
       | Unfold_nth c -> reduce (Unfold [AllOccurrences,c]) onConcl
       | Extern tacast -> conclPattern concl (FullHint.pattern h) tacast
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 0a213d5d0e..7a5615dd8e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -135,20 +135,20 @@ type 'a with_uid = {
   uid : KerName.t;
 }
 
-type raw_hint = constr * types * Univ.ContextSet.t
+type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *)
 
 type hint = {
   hint_term : constr;
   hint_type : types;
   hint_uctx : Univ.ContextSet.t;
   hint_clnv : clausenv;
+  hint_poly : bool;
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
 }
 
 type 'a with_metadata =
   { pri     : int
   (** A number lower is higher priority *)
-  ; poly    : bool
-  (** Is the hint polymorpic and hence should be refreshed at each application *)
   ; pat     : constr_pattern option
   (** A pattern for the concl of the Goal *)
   ; name    : hints_path_atom
@@ -305,14 +305,14 @@ let strip_params env sigma c =
   | _ -> c
 
 let instantiate_hint env sigma p =
-  let mk_clenv (c, cty, ctx) =
+  let mk_clenv (c, cty, ctx, poly) =
     let sigma = Evd.merge_context_set univ_flexible sigma ctx in
     let cl = mk_clenv_from_env env sigma None (c,cty) in
     let cl = {cl with templval =
           { cl.templval with rebus = strip_params env sigma cl.templval.rebus };
         env = empty_env}
     in
-    { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
+    { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly }
   in
   let code = match p.code.obj with
     | Res_pf c -> Res_pf (mk_clenv c)
@@ -806,9 +806,9 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
         | None -> pat
         in
         (Some hd,
-         { pri; poly; pat = Some pat; name;
+         { pri; pat = Some pat; name;
            db = None; secvars;
-           code = with_uid (Give_exact (c, cty, ctx)); })
+           code = with_uid (Give_exact (c, cty, ctx, poly)); })
 
 let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
@@ -830,10 +830,10 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
     in
     if Int.equal nmiss 0 then
       (Some hd,
-       { pri; poly; pat = Some pat; name;
+       { pri; pat = Some pat; name;
          db = None;
          secvars;
-         code = with_uid (Res_pf(c,cty,ctx)); })
+         code = with_uid (Res_pf(c,cty,ctx,poly)); })
     else begin
       if not eapply then failwith "make_apply_entry";
       if verbose then begin
@@ -849,9 +849,9 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (
         )
       end;
       (Some hd,
-       { pri; poly; pat = Some pat; name;
+       { pri; pat = Some pat; name;
          db = None; secvars;
-         code = with_uid (ERes_pf(c,cty,ctx)); })
+         code = with_uid (ERes_pf(c,cty,ctx,poly)); })
     end
   | _ -> failwith "make_apply_entry"
 
@@ -922,7 +922,6 @@ let make_unfold eref =
   let g = global_of_evaluable_reference eref in
   (Some g,
    { pri = 4;
-     poly = false;
      pat = None;
      name = PathHints [g];
      db = None;
@@ -933,7 +932,6 @@ let make_extern pri pat tacast =
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
-     poly = false;
      pat = pat;
      name = PathAny;
      db = None;
@@ -960,12 +958,11 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from_env env sigma None (c,t) in
   (Some hd,
    { pri=1;
-     poly = poly;
      pat = Some (Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma (clenv_type ce)));
      name = name;
      db = None;
      secvars = secvars_of_constr env sigma c;
-     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
+     code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) })
 
 
 
@@ -1076,29 +1073,30 @@ let subst_autohint (subst, obj) =
       (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
        with Bound -> gr')
   in
+  let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
+  let subst_aux ((c, t, ctx, poly) as h) =
+    let c' = subst_mps subst c in
+    let t' = subst_mps subst t in
+    if c==c' && t'==t then h else (c', t', ctx, poly)
+  in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
-    let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
-      | Res_pf (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code.obj else Res_pf (c', t',ctx)
-      | ERes_pf (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'==t then data.code.obj else ERes_pf (c',t',ctx)
-      | Give_exact (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t'== t then data.code.obj else Give_exact (c',t',ctx)
-      | Res_pf_THEN_trivial_fail (c,t,ctx) ->
-          let c' = subst_mps subst c in
-          let t' = subst_mps subst t in
-          if c==c' && t==t' then data.code.obj else Res_pf_THEN_trivial_fail (c',t',ctx)
+      | Res_pf h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Res_pf h'
+      | ERes_pf h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else ERes_pf h'
+      | Give_exact h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Give_exact h'
+      | Res_pf_THEN_trivial_fail h ->
+        let h' = subst_aux h in
+        if h == h' then data.code.obj else Res_pf_THEN_trivial_fail h'
       | Unfold_nth ref ->
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code.obj else Unfold_nth ref'
@@ -1587,7 +1585,6 @@ module FullHint =
 struct
   type t = full_hint
   let priority (h : t) = h.pri
-  let is_polymorphic (h : t) = h.poly
   let pattern (h : t) = h.pat
   let database (h : t) = h.db
   let run (h : t) k = run_hint h.code k
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 29fd90d3ef..8243716624 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -44,6 +44,7 @@ type hint = {
   hint_type : types;
   hint_uctx : Univ.ContextSet.t;
   hint_clnv : clausenv;
+  hint_poly : bool;
 }
 
 type 'a hints_path_atom_gen =
@@ -58,7 +59,6 @@ module FullHint :
 sig
   type t
   val priority : t -> int
-  val is_polymorphic : t -> bool
   val pattern : t -> Pattern.constr_pattern option
   val database : t -> string option
   val run : t -> (hint hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic
-- 
cgit v1.2.3


From 1d64f9d3ba9c529f2ff14198c94c9ffb3128afd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 13 Jun 2020 13:52:42 +0200
Subject: Add overlays.

---
 dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh

diff --git a/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
new file mode 100644
index 0000000000..ced0d95945
--- /dev/null
+++ b/dev/ci/user-overlays/12505-ppedrot-factor-hint-flags.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12505" ] || [ "$CI_BRANCH" = "factor-hint-flags" ]; then
+
+    fiat_parsers_CI_REF="factor-hint-flags"
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
-- 
cgit v1.2.3