diff options
| -rw-r--r-- | tactics/class_tactics.ml | 1 | ||||
| -rw-r--r-- | tactics/hints.ml | 1 | ||||
| -rw-r--r-- | tactics/hints.mli | 1 |
3 files changed, 0 insertions, 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 |