diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-08 12:00:56 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 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 |