diff options
| author | Pierre-Marie Pédrot | 2018-09-10 15:41:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-10 15:41:25 +0200 |
| commit | 2e931a4537aadfa4c15359c7b89ce4cb0291dad3 (patch) | |
| tree | 5e8df080a85734db4d3fd63e72acc5910200d6bb | |
| parent | 90a0357108769355025e8f15a6fbf6766aed8d44 (diff) | |
| parent | a488da64eb852554e0f1e60e2c94ea8cfc525dd7 (diff) | |
Merge PR #7743: Bound proof-search in default program obligation tactic.
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | theories/Program/Tactics.v | 2 |
2 files changed, 5 insertions, 1 deletions
@@ -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. |