diff options
author | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2008-07-25 15:12:53 +0200 |
commit | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch) | |
tree | dabcac548e299fee1da464c93b3dba98484f45b1 /contrib/subtac/Utils.v | |
parent | 2281410e38ef99d025ea77194585a9bc019fdaa9 (diff) |
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/subtac/Utils.v')
-rw-r--r-- | contrib/subtac/Utils.v | 65 |
1 files changed, 0 insertions, 65 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v deleted file mode 100644 index 76f49dd3..00000000 --- a/contrib/subtac/Utils.v +++ /dev/null @@ -1,65 +0,0 @@ -Require Export Coq.subtac.SubtacTactics. - -Set Implicit Arguments. - -(** Wrap a proposition inside a subset. *) - -Notation " {{ x }} " := (tt : { y : unit | x }). - -(** A simpler notation for subsets defined on a cartesian product. *) - -Notation "{ ( x , y ) : A | P }" := - (sig (fun anonymous : A => let (x,y) := anonymous in P)) - (x ident, y ident) : type_scope. - -(** Generates an obligation to prove False. *) - -Notation " ! " := (False_rect _ _). - -(** Abbreviation for first projection and hiding of proofs of subset objects. *) - -Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. -Notation "( x & ? )" := (@exist _ _ x _) : core_scope. - -(** Coerces objects to their support before comparing them. *) - -Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70). - -(** Quantifying over subsets. *) - -Notation "'fun' { x : A | P } => Q" := - (fun x:{x:A|P} => Q) - (at level 200, x ident, right associativity). - -Notation "'forall' { x : A | P } , Q" := - (forall x:{x:A|P}, Q) - (at level 200, x ident, right associativity). - -Require Import Coq.Bool.Sumbool. - -(** Construct a dependent disjunction from a boolean. *) - -Notation "'dec'" := (sumbool_of_bool) (at level 0). - -(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) - -Notation in_right := (@right _ _ _). -Notation in_left := (@left _ _ _). - -(** Default simplification tactic. *) - -Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; - try (solve [ red ; intros ; discriminate ]) ; auto with *. - -(** Extraction directives *) -Extraction Inline proj1_sig. -Extract Inductive unit => "unit" [ "()" ]. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -(* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) -(* Extract Inductive sigT => "prod" [ "" ]. *) - -Require Export ProofIrrelevance. -Require Export Coq.subtac.Heq. - -Delimit Scope program_scope with program. |