From ba88e99d37817cd3a591b14bbceb61e28f3e3382 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 27 Apr 2017 17:26:17 +0200
Subject: Aligning on standard layout of CHANGES.

---
 CHANGES | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index 8cb5573b21..69271f932e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -17,13 +17,12 @@ Tactics
     Most notably, the new implementation recognizes Miller patterns that were
     missed before because of a missing normalization step. Hopefully this should
     be fairly uncommon.
-- "auto with real" can now discharge comparisons of literals
+- Tactic "auto with real" can now discharge comparisons of literals.
 - The types of variables in patterns of "match" are now
   beta-iota-reduced after type-checking. This has an impact on the
   type of the variables that the tactic "refine" introduces in the
   context, producing types a priori closer to the expectations.
 
-
 Standard Library
 
 - New file PropExtensionality.v to explicitly work in the axiomatic
-- 
cgit v1.2.3