diff options
| author | Pierre-Marie Pédrot | 2019-04-02 18:50:05 +0200 |
|---|---|---|
| committer | GitHub | 2019-04-02 18:50:05 +0200 |
| commit | dc903c82c2308ae638147c5428511abe9279bf6d (patch) | |
| tree | 8e739bb2df6399e4f4ac29203898eee740843902 /src | |
| parent | ab24e0190e3b6a69b54ad62a63238906caeb0b11 (diff) | |
| parent | 9788d6d3b2799e5aeabaa4fbde9ae50d71f8b39b (diff) | |
Merge pull request coq/ltac2#118 from vbgl/rm-hardwired-hint-db
Fix for https://github.com/coq/coq/pull/8984
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 0c8522f495..ce37a613b1 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -405,7 +405,7 @@ let eauto debug n p lems dbs = let typeclasses_eauto strategy depth dbs = let only_classes, dbs = match dbs with | None -> - true, [Hints.typeclasses_db] + true, [Class_tactics.typeclasses_db] | Some dbs -> let dbs = List.map Id.to_string dbs in false, dbs |