diff options
Diffstat (limited to 'tactics/auto.mli')
| -rw-r--r-- | tactics/auto.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/auto.mli b/tactics/auto.mli index 094030beab..de1d2ff6b4 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -96,8 +96,8 @@ type hint_db_name = string type hint_db = Hint_db.t type hints_entry = - | HintsResolveEntry of (int option * bool * hints_path_atom * constr) list - | HintsImmediateEntry of (hints_path_atom * constr) list + | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference) list + | HintsImmediateEntry of (hints_path_atom * global_reference) list | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool |