diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-24 14:23:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-01-24 14:23:23 +0000 |
| commit | c155e42cdd1dd70b9e20243a6dc599ec653aef7a (patch) | |
| tree | 38b5b2100373b3e94b11c7b6f7ebed987ce20fc7 /contrib/subtac/Utils.v | |
| parent | baa006bc1d14f77fc8477cff25f22d5074b1f991 (diff) | |
Update some tests and fix section bug.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9530 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/subtac/Utils.v')
| -rw-r--r-- | contrib/subtac/Utils.v | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 412d5ae3b..34d9f6206 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -6,6 +6,8 @@ Notation "'fun' { x : A | P } => Q" := Notation "( x & ? )" := (@exist _ _ x _) : core_scope. +Notation " ! " := (False_rect _ _). + Definition ex_pi1 (A : Prop) (P : A -> Prop) (t : ex P) : A. intros. induction t. @@ -44,7 +46,7 @@ end. Ltac destruct_exists := repeat (destruct_one_pair) . -Ltac subtac_simpl := hnf ; intros ; destruct_exists ; try subst. +Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; auto. (* Destructs calls to f in hypothesis or conclusion, useful if f creates a subset object *) Ltac destruct_call f := |