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/hints.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.mli')

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(-)

(limited to 'tactics/hints.mli')

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.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'tactics/hints.mli')

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.

---
 tactics/hints.mli | 58 ++++++++++++++++++++++---------------------------------
 1 file changed, 23 insertions(+), 35 deletions(-)

(limited to 'tactics/hints.mli')

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/hints.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tactics/hints.mli')

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.

---
 tactics/hints.mli | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

(limited to 'tactics/hints.mli')

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/hints.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/hints.mli')

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