diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-26 00:33:43 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-08-26 00:33:43 +0000 |
| commit | 477bdffdb642698143f7da856e75db1dbe30653d (patch) | |
| tree | 6d78158e079ffe228cd78bd7159ef2473f478463 /theories/Program/Tactics.v | |
| parent | 6efaa1f45a855418d0bc7c8656e4ed83778903ee (diff) | |
Add more equality tactics. Upgrade program_simpl for discrimination of conjuncts.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10093 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Tactics.v')
| -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 d5ccdf1c5..dfe8453d1 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -162,4 +162,4 @@ Tactic Notation "dependent" "induction" ident(H) "generalizing" ne_hyp_list(l) : (** The default simplification tactic used by Program. *) Ltac program_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; - try (solve [ red ; intros ; discriminate ]) ; auto with *. + try (solve [ red ; intros ; destruct_conjs ; discriminate ]) ; auto with *. |