diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Tactics.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index b3b08e067b..75aa5eb7cf 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -308,6 +308,11 @@ Ltac program_simplify := subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_simpl := program_simplify ; auto. +Ltac program_solve_wf := + match goal with + |- well_founded _ => auto with * + end. + +Ltac program_simpl := program_simplify ; auto; try program_solve_wf. Obligation Tactic := program_simpl. |