From 880fee8f80503fc8a40e2e07b565cfd2a99d24da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 19 Apr 2018 10:30:08 +0200
Subject: Make "intro"/"intros" progress on existential variables.

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index a270aef96d..68cc495f58 100644
--- a/CHANGES
+++ b/CHANGES
@@ -19,6 +19,12 @@ Vernacular Commands
 - Removed deprecated commands Arguments Scope and Implicit Arguments
   (not the option). Use the Arguments command instead.
 
+Tactics
+
+- Introduction tactics "intro"/"intros" on a goal which is an
+  existential variable now force a refinement of the goal into a
+  dependent product rather than failing.
+
 Tactic language
 
 - Support for fix/cofix added in Ltac "match" and "lazymatch".
-- 
cgit v1.2.3