diff options
Diffstat (limited to 'tactics/hints.ml')
| -rw-r--r-- | tactics/hints.ml | 1 |
1 files changed, 0 insertions, 1 deletions
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 |