From 5c07e11226e44dadb04a2fe48c91cce094989ce0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 8 Oct 2016 12:00:56 +0200
Subject: Report about changes of semantics of auto as an ltac argument (see
 #4966).

---
 CHANGES | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/CHANGES b/CHANGES
index 6ea680153d..0210281c3a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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
 
-- 
cgit v1.2.3