diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-03 08:59:59 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-03 08:59:59 +0000 |
commit | eefe264e275ae4e59389957ea2df7ef75f451c76 (patch) | |
tree | 5b82e06ba7531117753081f3f777734c8b5c1203 /theories | |
parent | fe3f4a3df7a422208d86532c24112b8f22065fab (diff) |
Nouveau fichier Tactics.v collectant les tactiques utiles des utilisateurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6666 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Init/Tactics.v | 23 |
1 files changed, 23 insertions, 0 deletions
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v new file mode 100644 index 000000000..fcdbc6e87 --- /dev/null +++ b/theories/Init/Tactics.v @@ -0,0 +1,23 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id$ i*) + +Require Import Notations. +Require Import Logic. + +(** Useful tactics *) + +Ltac rewrite_all Eq := match type of Eq with + ?a = ?b => + generalize Eq; clear Eq; + match goal with + | H : context [a] |- _ => intro Eq; rewrite Eq in H; rewrite_all Eq + | _ => intro Eq + end + end. |