From a488da64eb852554e0f1e60e2c94ea8cfc525dd7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 8 Jun 2018 13:12:19 +0200
Subject: Bound proof-search in default program obligation tactic.

This issue was first reported on equations where a definition seemingly
took all memory until Coq crashed.

https://github.com/mattam82/Coq-Equations/issues/69
---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 5d1c9a9c2d..0ccbb10657 100644
--- a/CHANGES
+++ b/CHANGES
@@ -34,6 +34,10 @@ Tactics
 
 - Deprecated the Implicit Tactic family of commands.
 
+- The default program obligation tactic uses a bounded proof search
+  instead of an unbounded and potentially non-terminating one now
+  (source of incompatibility).
+
 - The `simple apply` tactic now respects the `Opaque` flag when called from
   Ltac (`auto` still does not respect it).
 
-- 
cgit v1.2.3