diff options
| -rw-r--r-- | tactics/hints.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/hints.mli b/tactics/hints.mli index 42379b7c0c..9a781c722c 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -54,8 +54,7 @@ type search_entry (** The head may not be bound. *) -type hint_entry = global_reference option * - (constr * types * Univ.universe_context_set) gen_auto_tactic +type hint_entry type hints_path = | PathAtom of hints_path_atom |