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 a4933a8963..0d5d275384 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -441,7 +441,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 Constrintern.add_glob (loc_of_reference r) gr; + if !Flags.dump then Dumpglob.add_glob (loc_of_reference r) gr; (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> |