doc and CHANGELOG

CHANGELOG_UNRELEASED.md

@@ -18,6 +18,162 @@
 
 - in `normedtype.v`:
   + hints for `at_right_proper_filter` and `at_left_proper_filter`
+- in `sequences.v`:
+  + lemma `invr_cvg0` and `invr_cvg_pinfty`
+  + lemma `cvgPninfty_lt`, `cvgPpinfty_near`, `cvgPninfty_near`,
+    `cvgPpinfty_lt_near` and `cvgPninfty_lt_near`
+- in `classical_sets.v`:
+  + notations `\bigcup_(i < n) F` and `\bigcap_(i < n) F`
+
+- in `boolp.v`:
+  + tactic `eqProp`
+  + definition `BoolProp`
+  + lemmas `PropB`, `notB`, `andB`, `orB`, `implyB`, `decide_or`, `not_andE`,
+    `not_orE`, `orCA`, `orAC`, `orACA`, `orNp`, `orpN`, `or3E`, `or4E`, `andCA`,
+	 `andAC`, `andACA`, `and3E`, `and4E`, `and5E`, `implyNp`, `implypN`,
+	 `implyNN`, `or_andr`, `or_andl`, `and_orr`, `and_orl`, `exists2E`,
+	 `inhabitedE`, `inhabited_witness`
+
+- file `contra.v`
+- in `contra.v`
+  + definitions `move_view`, `move_viewP`, `forallSort`
+  + notation `mkForallSort`
+  + definitions `TypeForall`, `PropForall`, `SetForall`, `Forall`
+  + notation `\Forall x .. z, T`
+  + tactic notation `ForallI`
+  + definitions `wrappedProp`, `wrap4Prop`, `wrap3Prop`, `wrap2Prop`,
+    `wrap1Prop`, `wrappedType`, `wrap4Type`, `wrap3Type`, `wrap2Type`,
+    `wrap1Type`
+  + lemma `generic_forall_extensionality`
+  + definitions `negatedProp`, `properNegatedProp`
+  + lemmas `lax_notE`, `lax_notP`
+  + definitions `notE`, `notP`
+  + lemma `proper_nPropP`
+  + definitions `notI`, `proper_nProp`, `trivial_nProp`, `True_nProp`,
+    `False_nProp`, `not_nProp`
+  + lemma `and_nPropP`
+  + definition `and_nProp`
+  + lemma `and3_nPropP`
+  + definition `and3_nProp`
+  + lemma `and4_nPropP`
+  + definition `and4_nProp`
+  + lemma `and5_nPropP`
+  + definition `and5_nProp`
+  + lemma `or_nPropP`
+  + definition `or_nProp`
+  + lemma `or3_nPropP`
+  + definition `or3_nProp`
+  + lemma `or4_nPropP`
+  + definition `or4_nProp`
+  + notation `and_def binary P Q PQ`
+  + definitions `andRHS`, `unary_and_rhs`, `binary_and_rhs`
+  + lemma `imply_nPropP`
+  + definition `imply_nProp`
+  + lemma `exists_nPropP`
+  + definition `exists_nProp`
+  + lemma `exists2_nPropP`
+  + definition `exists2_nProp`
+  + lemma `inhabited_nPropP`
+  + definitions `inhabited_nProp`, `negatedForallBody`,
+    `properNegatedForallBody`
+  + notation `nBody b P nQ t nR x`
+  + lemma `forall_nPropP`
+  + definition `forall_nProp`
+  + lemma `proper_nBodyP`
+  + definition `proper_nBody`, `nonproper_nBody`
+  + lemma `andRHS_def`
+  + definitions `bounded_nBody`, `unbounded_nBody`, `negatedBool`,
+    `positedBool`
+  + lemma `is_true_nPropP`
+  + definition `is_true_nProp`
+  + lemmas `true_negP`, `true_posP`, `false_negP`, `false_posP`
+  + definitions `true_neg`, `true_pos`, `false_neg`, `false_pos`
+  + lemma `id_negP`
+  + definitions `id_neg`, `id_pos`
+  + lemma `negb_negP`
+  + definition `negb_neg`
+  + lemma `negb_posP`
+  + definitions `negb_pos`, `negatedLeqLHS`, `neg_ltn_LHS`, `neg_leq_LHS`
+  + lemma `leq_negP`
+  + definitions `leq_neg`, `neqRHS`, `boolNeqRHS`
+  + lemma `eq_nPropP`
+  + definition `eq_nProp`
+  + lemma `bool_neqP`
+  + definitions `bool_neq`, `true_neq`
+  + lemma `false_neqP`
+  + definition `false_neq`
+  + lemma `eqType_neqP`
+  + definition `eqType_neq`
+  + lemma `eq_op_posP`
+  + definitionss `eq_op_pos`, `witnessedType`, `properWitnessedType`
+  + lemmas `witnessedType_intro`, `witnessedType_elim`, `eq_inhabited`
+  + definition `Prop_wType`
+  + lemma `proper_wTypeP`
+  + definition `proper_wType`
+  + lemma `forall_wTypeP`
+  + definitions `forall_wType`, `inhabited_wType`
+  + lemma `void_wTypeP`
+  + definition `void_wType`
+  + lemma `unit_wTypeP`
+  + definition `unit_wType`
+  + lemma `pair_wTypeP`
+  + definition `pair_wType`
+  + lemma `sum_wTypeP`
+  + definition `sum_wTypeP`
+  + lemma `sumbool_wTypeP`
+  + definition `sumbool_wType`
+  + lemma `sumor_wTypeP`
+  + definition `sumor_wType`
+  + lemma `sig1_wTypeP`
+  + definition `sig1_wType`
+  + lemma `sig2_wTypeP`
+  + definition `sig2_wType`
+  + lemma `sigT_wTypeP`
+  + definition `sigT_wType`
+  + lemma `sigT2_wTypeP`
+  + definitions `sigT2_wType`, `witnessProp`, `properWitnessProp`
+  + lemmas `wPropP`, `lax_witness`
+  + definition `witness`
+  + lemma `proper_wPropP`
+  + definition `proper_wProp`
+  + lemma `forall_wPropP`
+  + definitions `forall_wProp`, `trivial_wProp`, `inhabited_wProp`, `nandBool`,
+    `nand_false_bool`, `nand_true_bool`
+  + lemma `and_wPropP`
+  + definition `and_wProp`
+  + lemma `or_wPropP`
+  + definition `or_wProp`
+  + lemma `exists_wPropP`
+  + definition `exists_wProp`
+  + lemma `exists2_wPropP`
+  + definition `exists2_wProp`
+  + lemma `push_goal_copy`, `assume_not_with`, `absurdW`, `contra_Type`,
+    `contra_notP`, `assume_not`
+  + tactic `assume_not`
+  + lemma `absurd_not`
+  + tactics `absurd_not`, `contrapose`
+  + tactic notations `contra`, `contra : constr(H)`, `contra : ident(H)`,
+    `contra : { hyp_list(Hs) } constr(H)`, `contra : { hyp_list(Hs) } ident(H)`,
+	 `contra : { - } constr(H)`
+  + lemma `absurd`
+  + tactic notations `absurd`, `absurd constr(P)`, `absurd : constr(H)`,
+    `absurd : ident(H)`, `absurd : { hyp_list(Hs) } constr(H)`,
+	 `absurd : { hyp_list(Hs) } ident(H)`
+
+### Changed
+- in `topology.v`
+  + definition `fct_restrictedUniformType` changed to use `weak_uniformType`
+  + definition `family_cvg_topologicalType` changed to use `sup_uniformType`
+
+- in `constructive_ereal.v`:
+  + lemmas `lee_paddl`, `lte_paddl`, `lee_paddr`, `lte_paddr`,
+    `lte_spaddr`, `lee_pdaddl`, `lte_pdaddl`, `lee_pdaddr`,
+    `lte_pdaddr`, `lte_spdaddr` generalized to `realDomainType`
+- in `constructive_ereal.v`:
+  + generalize `lte_addl`, `lte_addr`, `gte_subl`, `gte_subr`,
+    `lte_daddl`, `lte_daddr`, `gte_dsubl`, `gte_dsubr`
+- in `topology.v`:
+  + lemmas `continuous_subspace0`, `continuous_subspace1`
 
 - in `realfun.v`:
   + notations `nondecreasing_fun`, `nonincreasing_fun`,
@@ -76,6 +232,9 @@
 	`ae_eq_mul1l`,
 	`ae_eq_abse`
 
+-in `boolp.v`
+  - lemmas `orC` and `andC` now use `commutative`
+
 ### Renamed
 
 - in `exp.v`: