diff options
| author | Matthieu Sozeau | 2018-06-08 13:12:19 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-09-06 16:43:38 +0200 |
| commit | a488da64eb852554e0f1e60e2c94ea8cfc525dd7 (patch) | |
| tree | e24903bd36134020a382b9b3d8ca9a956bd05448 /theories/Program | |
| parent | 51197c3b8b5a6f30397f0263e2e2f4461519c66e (diff) | |
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
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Tactics.v | 2 |
1 files changed, 1 insertions, 1 deletions
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. |