diff options
| author | Hugo Herbelin | 2016-10-08 12:00:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-10-08 12:02:13 +0200 |
| commit | 5c07e11226e44dadb04a2fe48c91cce094989ce0 (patch) | |
| tree | 3198da92f366591d220abba9a932f1401bbfe05a | |
| parent | 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 (diff) | |
Report about changes of semantics of auto as an ltac argument (see #4966).
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 3 insertions, 0 deletions
@@ -14,6 +14,9 @@ Bugfixes binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. - #3070: fixing "subst" in the presence of a chain of dependencies. +- When used as an argument of an ltac function, "auto" without "with" + nor "using" clause now correctly uses only the core hint database by + default. Specification language |