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

(limited to 'theories/Program')

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