diff options
author | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-06-04 12:07:52 +0200 |
commit | 61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch) | |
tree | d88d05baf35b9b09a034233300f35a694f9fa6c2 /theories/Init | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'theories/Init')
-rw-r--r-- | theories/Init/Logic.v | 4 | ||||
-rw-r--r-- | theories/Init/Prelude.v | 1 | ||||
-rw-r--r-- | theories/Init/Specif.v | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index d1eabcab..9cd0b31b 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -221,7 +221,7 @@ Definition all (A:Type) (P:A -> Prop) := forall x:A, P x. Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) (at level 200, x binder, right associativity, - format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' '/ ' x .. y , '/ ' p ']'") : type_scope. Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q)) @@ -404,7 +404,7 @@ Definition uniqueness (A:Type) (P:A->Prop) := forall x y, P x -> P y -> x = y. Notation "'exists' ! x .. y , p" := (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) (at level 200, x binder, right associativity, - format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") + format "'[' 'exists' ! '/ ' x .. y , '/ ' p ']'") : type_scope. Lemma unique_existence : forall (A:Type) (P:A->Prop), diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v index e929c561..d85f5363 100644 --- a/theories/Init/Prelude.v +++ b/theories/Init/Prelude.v @@ -19,7 +19,6 @@ Declare ML Module "extraction_plugin". Declare ML Module "decl_mode_plugin". Declare ML Module "cc_plugin". Declare ML Module "ground_plugin". -Declare ML Module "dp_plugin". Declare ML Module "recdef_plugin". Declare ML Module "subtac_plugin". Declare ML Module "xml_plugin". diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 637994b2..5b7afc99 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -60,7 +60,7 @@ Add Printing Let sigT2. (** Projections of [sig] - An element [y] of a subset [{x:A & (P x)}] is the pair of an [a] + An element [y] of a subset [{x:A | (P x)}] is the pair of an [a] of type [A] and of a proof [h] that [a] satisfies [P]. Then [(proj1_sig y)] is the witness [a] and [(proj2_sig y)] is the proof of [(P a)] *) |