diff options
| author | Pierre-Marie Pédrot | 2015-04-12 21:13:51 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-04-12 21:13:51 +0200 |
| commit | 91172e9c3a1430c3be3ad1080d2da68b25d940aa (patch) | |
| tree | d4a0497e364036e559283afee26634806d2fb120 | |
| parent | b3192497979a57a6078b2ecdb0d8b546cb100ffa (diff) | |
Making the hint entry type opaque.
| -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 |