aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-02-17 16:14:28 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-02-17 16:14:28 +0000
commit18c1f91426baea8fdce67a1a6b41a1ab106f93ee (patch)
tree6e1dd345350e2e5eea25348d3dea646f6ff5d154 /theories
parentb63f3d7db6e23746165f2a8501dfc3b52351530b (diff)
In Program obligation, do not use auto on non-proposition goals by
default. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13845 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r--theories/Program/Tactics.v9
1 files changed, 7 insertions, 2 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 38788cbc5..3eec32620 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -306,11 +306,16 @@ simpl in |- *; intros ; destruct_all_rec_calls ; repeat (destruct_conjs; simpl p
subst*; autoinjections ; try discriminates ;
try (solve [ red ; intros ; destruct_conjs ; autoinjections ; discriminates ]).
+(** Restrict automation to propositional obligations. *)
+
Ltac program_solve_wf :=
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.
+Create HintDb program discriminated.
+
+Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf.
Obligation Tactic := program_simpl.