From 89a85a6603b7112e685a052d728284d3e4c2881e Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 11 May 2018 23:07:14 +0200
Subject: Fix #7421: constr_eq ignores universe constraints.

The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
---
 CHANGES | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index ce8e313b99..c36f59726b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,12 @@ Tactics
 - The `simple apply` tactic now respects the `Opaque` flag when called from
   Ltac (`auto` still does not respect it).
 
+- Tactic `constr_eq` now adds universe constraints needed for the
+  identity to the context (it used to ignore them). New tactic
+  `constr_eq_strict` checks that the required constraints already hold
+  without adding new ones. Preexisting tactic `constr_eq_nounivs` can
+  still be used if you really want to ignore universe constraints.
+
 Tools
 
 - Coq_makefile lets one override or extend the following variables from
-- 
cgit v1.2.3