diff options
| author | Maxime Dénès | 2019-04-26 09:41:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-02 12:30:34 +0200 |
| commit | 48b86574606b9500864a79ddc6a0a668e1aaf295 (patch) | |
| tree | ff2661c80891efda2790741d9c14f22baebe511d | |
| parent | afb58502f900554986aeee9a749871630f117edd (diff) | |
Remove outdated comment
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 575c1dba46..160e4f164e 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -991,8 +991,6 @@ module Search = struct typeclasses_eauto env evd ?depth unique (modes,st) [db] p end -(** Binding to either V85 or Search implementations. *) - let typeclasses_eauto ?(only_classes=false) ?(st=TransparentState.full) ?strategy ~depth dbs = let dbs = List.map_filter |