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 ++++
 theories/Program/Tactics.v | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

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).
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index bc83881849..edbae6534a 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -326,7 +326,7 @@ Ltac program_solve_wf :=
 
 Create HintDb program discriminated.
 
-Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf.
+Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf.
 
 Obligation Tactic := program_simpl.
 
-- 
cgit v1.2.3