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