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

1 files changed, 4 insertions, 0 deletions

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).