diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 1c3e2ce086..6641289eb5 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -478,7 +478,7 @@ let add_hints local dbnames0 h = (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference.") in - if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; + if Dumpglob.dump () then Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> |