From a0d3865ced307d6f826b2eaae9cc2e23ff465d8b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 28 Mar 2018 17:52:17 +0200
Subject: Supporting fix/cofix in Ltac pattern-matching (wish #7092).

This is done by not failing for fix/cofix while translating from
glob_constr to constr_pattern.
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 24c4cfec0..8805254b1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -6,6 +6,10 @@ Tools
 - Coq_makefile lets one override or extend the following variables from
   the command line: COQFLAGS, COQCHKFLAGS, COQDOCFLAGS.
 
+Tactic language
+
+- Support for fix/cofix added in Ltac "match" and "lazymatch".
+
 Changes from 8.7.2 to 8.8+beta1
 ===============================
 
-- 
cgit v1.2.3