diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
| commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
| tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 /theories/Program/Tactics.v | |
| parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) | |
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'theories/Program/Tactics.v')
| -rw-r--r-- | theories/Program/Tactics.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 333dd7a6..4a41d9c9 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 13332 2010-07-26 22:12:43Z msozeau $ i*) +(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) @@ -308,11 +308,14 @@ Ltac program_simplify := subst*; autoinjections ; try discriminates ; try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]). -Ltac program_solve_wf := +(** We only try to solve proposition goals automatically. *) + +Ltac program_solve := match goal with - |- well_founded _ => auto with * + | |- well_founded _ => auto with * + | |- ?T => match type of T with Prop => auto end end. -Ltac program_simpl := program_simplify ; auto; try program_solve_wf. +Ltac program_simpl := program_simplify ; try program_solve. Obligation Tactic := program_simpl. |