diff options
| author | Hugo Herbelin | 2014-10-07 17:26:02 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-07 18:40:36 +0200 |
| commit | 38b34dfffcceab7fa7d5ba43c84e414d24cebe43 (patch) | |
| tree | c5449cf9c02c97586bf8a8edaa52d05d876d3e94 /tactics/g_class.ml4 | |
| parent | 2313bde0116a5916912bebbaca77d291f7b2760a (diff) | |
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
being able to export hints without tactics, vm, etc. to come with.
Some functions moved to the new proof engine.
Diffstat (limited to 'tactics/g_class.ml4')
| -rw-r--r-- | tactics/g_class.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/g_class.ml4 b/tactics/g_class.ml4 index 1e666e5a55..a49c76f148 100644 --- a/tactics/g_class.ml4 +++ b/tactics/g_class.ml4 @@ -64,7 +64,7 @@ END TACTIC EXTEND typeclasses_eauto | [ "typeclasses" "eauto" "with" ne_preident_list(l) ] -> [ Proofview.V82.tactic (typeclasses_eauto l) ] -| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Auto.typeclasses_db]) ] +| [ "typeclasses" "eauto" ] -> [ Proofview.V82.tactic (typeclasses_eauto ~only_classes:true [Hints.typeclasses_db]) ] END TACTIC EXTEND head_of_constr |