diff --git a/lf-current/AltAuto.html b/lf-current/AltAuto.html index 62c584eef..0b055f7ab 100644 --- a/lf-current/AltAuto.html +++ b/lf-current/AltAuto.html @@ -2410,7 +2410,7 @@

AltAutoA Streamlined Treatment of Au
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/AltAuto.v b/lf-current/AltAuto.v index 4f3a6d0c7..a36811112 100644 --- a/lf-current/AltAuto.v +++ b/lf-current/AltAuto.v @@ -1825,4 +1825,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None. - Ltac functions and [match goal] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/AltAutoTest.v b/lf-current/AltAutoTest.v index 80a8cd519..060bac814 100644 --- a/lf-current/AltAutoTest.v +++ b/lf-current/AltAutoTest.v @@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------". idtac "MANUAL". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Auto.html b/lf-current/Auto.html index 49a353976..a6964d5c8 100644 --- a/lf-current/Auto.html +++ b/lf-current/Auto.html @@ -910,7 +910,7 @@

AutoMore Automation

Proof.
  intros P Q HP HQ. destruct HP as [y HP']. eauto.
Qed.
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Auto.v b/lf-current/Auto.v index 2cc0af3be..54097eb70 100644 --- a/lf-current/Auto.v +++ b/lf-current/Auto.v @@ -740,4 +740,4 @@ Proof. intros P Q HP HQ. destruct HP as [y HP']. eauto. Qed. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/AutoTest.v b/lf-current/AutoTest.v index 2f499b37e..bcaa8f81a 100644 --- a/lf-current/AutoTest.v +++ b/lf-current/AutoTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Basics.html b/lf-current/Basics.html index e94b35413..900eb512c 100644 --- a/lf-current/Basics.html +++ b/lf-current/Basics.html @@ -2691,7 +2691,7 @@

BasicsFunctional Programming in Coq<
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Basics.v b/lf-current/Basics.v index 54cababee..750446c85 100644 --- a/lf-current/Basics.v +++ b/lf-current/Basics.v @@ -2015,4 +2015,4 @@ Example test_bin_incr6 : output. But since they have to be graded by a human, the test script won't be able to tell you much about them. *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/BasicsTest.v b/lf-current/BasicsTest.v index 971a51d25..89400695b 100644 --- a/lf-current/BasicsTest.v +++ b/lf-current/BasicsTest.v @@ -521,4 +521,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/Bib.html b/lf-current/Bib.html index 72a03a987..fd2783519 100644 --- a/lf-current/Bib.html +++ b/lf-current/Bib.html @@ -84,7 +84,7 @@

BibBibliography

-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Bib.v b/lf-current/Bib.v index cf55026f3..f5b658361 100644 --- a/lf-current/Bib.v +++ b/lf-current/Bib.v @@ -32,4 +32,4 @@ *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/BibTest.v b/lf-current/BibTest.v index a06a27e93..c9d1144f6 100644 --- a/lf-current/BibTest.v +++ b/lf-current/BibTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Extraction.html b/lf-current/Extraction.html index 6e2c81dc9..b6d035f7c 100644 --- a/lf-current/Extraction.html +++ b/lf-current/Extraction.html @@ -232,7 +232,7 @@

ExtractionExtracting OCaml from Coq<
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Extraction.v b/lf-current/Extraction.v index 2d1d5d91c..4dc542f7d 100644 --- a/lf-current/Extraction.v +++ b/lf-current/Extraction.v @@ -129,4 +129,4 @@ Extraction "imp.ml" empty_st ceval_step parse. chapter in _Verified Functional Algorithms_ (_Software Foundations_ volume 3). *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ExtractionTest.v b/lf-current/ExtractionTest.v index 5432cc667..515991f1c 100644 --- a/lf-current/ExtractionTest.v +++ b/lf-current/ExtractionTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Imp.html b/lf-current/Imp.html index 7bd05778d..18c250172 100644 --- a/lf-current/Imp.html +++ b/lf-current/Imp.html @@ -2861,7 +2861,7 @@

ImpSimple Imperative Programs
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Imp.v b/lf-current/Imp.v index d24ce1f8a..ccc2565c4 100644 --- a/lf-current/Imp.v +++ b/lf-current/Imp.v @@ -2077,4 +2077,4 @@ End BreakImp. [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ImpCEvalFun.html b/lf-current/ImpCEvalFun.html index 4c65b7868..1ad335f7a 100644 --- a/lf-current/ImpCEvalFun.html +++ b/lf-current/ImpCEvalFun.html @@ -481,7 +481,7 @@

ImpCEvalFunAn Evaluation Function fo
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/ImpCEvalFun.v b/lf-current/ImpCEvalFun.v index 1b7a5cb36..c08b47e2d 100644 --- a/lf-current/ImpCEvalFun.v +++ b/lf-current/ImpCEvalFun.v @@ -393,4 +393,4 @@ Proof. rewrite E1 in E2. inversion E2. reflexivity. lia. lia. Qed. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ImpCEvalFunTest.v b/lf-current/ImpCEvalFunTest.v index 2c65bc08e..7952a255e 100644 --- a/lf-current/ImpCEvalFunTest.v +++ b/lf-current/ImpCEvalFunTest.v @@ -91,4 +91,4 @@ idtac "---------- ceval_step__ceval_inf ---------". idtac "MANUAL". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/ImpParser.html b/lf-current/ImpParser.html index a18a0e51f..80733d0f6 100644 --- a/lf-current/ImpParser.html +++ b/lf-current/ImpParser.html @@ -536,7 +536,7 @@

ImpParserLexing and Parsing in Coqend;
      "x" := "z" }>.
Proof. cbv. reflexivity. Qed.
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/ImpParser.v b/lf-current/ImpParser.v index 16b801dc5..c0b9a4e25 100644 --- a/lf-current/ImpParser.v +++ b/lf-current/ImpParser.v @@ -462,4 +462,4 @@ Example eg2 : parse " "x" := "z" }>. Proof. cbv. reflexivity. Qed. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ImpParserTest.v b/lf-current/ImpParserTest.v index 976ee0321..fcf6880c5 100644 --- a/lf-current/ImpParserTest.v +++ b/lf-current/ImpParserTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/ImpTest.v b/lf-current/ImpTest.v index d3525d189..7c0fed4d2 100644 --- a/lf-current/ImpTest.v +++ b/lf-current/ImpTest.v @@ -314,4 +314,4 @@ idtac "---------- BreakImp.seq_stops_on_break ---------". Print Assumptions BreakImp.seq_stops_on_break. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/IndPrinciples.html b/lf-current/IndPrinciples.html index ba61c8f1b..05b82e844 100644 --- a/lf-current/IndPrinciples.html +++ b/lf-current/IndPrinciples.html @@ -1361,7 +1361,7 @@

IndPrinciplesInduction Principles -(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/IndPrinciples.v b/lf-current/IndPrinciples.v index 74d12b96f..06a464e97 100644 --- a/lf-current/IndPrinciples.v +++ b/lf-current/IndPrinciples.v @@ -963,4 +963,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/IndPrinciplesTest.v b/lf-current/IndPrinciplesTest.v index e36b02e69..ecd674111 100644 --- a/lf-current/IndPrinciplesTest.v +++ b/lf-current/IndPrinciplesTest.v @@ -109,4 +109,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/IndProp.html b/lf-current/IndProp.html index 7ffcc6da5..7bd374262 100644 --- a/lf-current/IndProp.html +++ b/lf-current/IndProp.html @@ -3320,7 +3320,7 @@

IndPropInductively Defined Propositi
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/IndProp.v b/lf-current/IndProp.v index dbaeaa86d..91c0e5b8a 100644 --- a/lf-current/IndProp.v +++ b/lf-current/IndProp.v @@ -2433,4 +2433,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/IndPropTest.v b/lf-current/IndPropTest.v index 6a1584641..c45979ec2 100644 --- a/lf-current/IndPropTest.v +++ b/lf-current/IndPropTest.v @@ -332,4 +332,4 @@ idtac "---------- merge_filter ---------". Print Assumptions merge_filter. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Induction.html b/lf-current/Induction.html index 08c8c0502..987932848 100644 --- a/lf-current/Induction.html +++ b/lf-current/Induction.html @@ -1075,7 +1075,7 @@

InductionProof by Induction -(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Induction.v b/lf-current/Induction.v index 438ff4b94..b6e4e4f18 100644 --- a/lf-current/Induction.v +++ b/lf-current/Induction.v @@ -774,4 +774,4 @@ Proof. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/InductionTest.v b/lf-current/InductionTest.v index 4c270b524..28d643e44 100644 --- a/lf-current/InductionTest.v +++ b/lf-current/InductionTest.v @@ -258,4 +258,4 @@ idtac "---------- bin_nat_bin ---------". Print Assumptions bin_nat_bin. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/Lists.html b/lf-current/Lists.html index 0f5391111..5428fd893 100644 --- a/lf-current/Lists.html +++ b/lf-current/Lists.html @@ -1522,7 +1522,7 @@

ListsWorking with Structured Data End PartialMap.
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Lists.v b/lf-current/Lists.v index 40357d6d5..1271df052 100644 --- a/lf-current/Lists.v +++ b/lf-current/Lists.v @@ -1137,4 +1137,4 @@ Proof. (** [] *) End PartialMap. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ListsTest.v b/lf-current/ListsTest.v index a457638f2..4b2ab3e4e 100644 --- a/lf-current/ListsTest.v +++ b/lf-current/ListsTest.v @@ -516,4 +516,4 @@ idtac "---------- NatList.rev_injective ---------". Print Assumptions NatList.rev_injective. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Logic.html b/lf-current/Logic.html index 97fde8333..86dfa88ce 100644 --- a/lf-current/Logic.html +++ b/lf-current/Logic.html @@ -2404,7 +2404,7 @@

LogicLogic in Coq

-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Logic.v b/lf-current/Logic.v index f79e0c13e..06ede98a2 100644 --- a/lf-current/Logic.v +++ b/lf-current/Logic.v @@ -1737,4 +1737,4 @@ Definition consequentia_mirabilis := forall P:Prop, [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/LogicTest.v b/lf-current/LogicTest.v index 5e4a63c81..b90555fa9 100644 --- a/lf-current/LogicTest.v +++ b/lf-current/LogicTest.v @@ -414,4 +414,4 @@ idtac "---------- not_exists_dist ---------". Print Assumptions not_exists_dist. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Maps.html b/lf-current/Maps.html index 292ef2471..f129f2bbc 100644 --- a/lf-current/Maps.html +++ b/lf-current/Maps.html @@ -562,7 +562,7 @@

MapsTotal and Partial Maps
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Maps.v b/lf-current/Maps.v index 451a13791..6a5b74152 100644 --- a/lf-current/Maps.v +++ b/lf-current/Maps.v @@ -379,4 +379,4 @@ Qed. used to keep track of which program variables are defined in a given scope. *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/MapsTest.v b/lf-current/MapsTest.v index 38ea114a9..b1e770860 100644 --- a/lf-current/MapsTest.v +++ b/lf-current/MapsTest.v @@ -94,4 +94,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Poly.html b/lf-current/Poly.html index f1416a074..90ec339bb 100644 --- a/lf-current/Poly.html +++ b/lf-current/Poly.html @@ -1735,7 +1735,7 @@

PolyPolymorphism and Higher-Order Fu End Church.
End Exercises.
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Poly.v b/lf-current/Poly.v index 2dc361593..2b4f663b3 100644 --- a/lf-current/Poly.v +++ b/lf-current/Poly.v @@ -1224,4 +1224,4 @@ Proof. (* FILL IN HERE *) Admitted. End Church. End Exercises. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/PolyTest.v b/lf-current/PolyTest.v index 980a2dad9..f691ee59d 100644 --- a/lf-current/PolyTest.v +++ b/lf-current/PolyTest.v @@ -498,4 +498,4 @@ idtac "---------- Exercises.Church.exp_3 ---------". Print Assumptions Exercises.Church.exp_3. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Postscript.html b/lf-current/Postscript.html index d77ba82e2..2e4485ca0 100644 --- a/lf-current/Postscript.html +++ b/lf-current/Postscript.html @@ -217,7 +217,7 @@

Postscript

-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Postscript.v b/lf-current/Postscript.v index e5065ba67..e45520dbc 100644 --- a/lf-current/Postscript.v +++ b/lf-current/Postscript.v @@ -82,4 +82,4 @@ {https://deepspec.org/event/dsss17/index.html} *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/PostscriptTest.v b/lf-current/PostscriptTest.v index 29386c580..59e838445 100644 --- a/lf-current/PostscriptTest.v +++ b/lf-current/PostscriptTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Preface.html b/lf-current/Preface.html index dd009c417..133bf35e1 100644 --- a/lf-current/Preface.html +++ b/lf-current/Preface.html @@ -755,7 +755,7 @@

Preface


-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Preface.v b/lf-current/Preface.v index 950c595e3..297c50c5d 100644 --- a/lf-current/Preface.v +++ b/lf-current/Preface.v @@ -506,4 +506,4 @@ NSF Expeditions grant 1521523, _The Science of Deep Specification_. *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/PrefaceTest.v b/lf-current/PrefaceTest.v index 0482d4c4f..9cb35c614 100644 --- a/lf-current/PrefaceTest.v +++ b/lf-current/PrefaceTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ProofObjects.html b/lf-current/ProofObjects.html index 1296ae00c..de1abca25 100644 --- a/lf-current/ProofObjects.html +++ b/lf-current/ProofObjects.html @@ -1304,7 +1304,7 @@

ProofObjectsThe Curry-Howard Corresp
-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/ProofObjects.v b/lf-current/ProofObjects.v index b3dcd5bb7..c5de08d89 100644 --- a/lf-current/ProofObjects.v +++ b/lf-current/ProofObjects.v @@ -921,4 +921,4 @@ Theorem pe_implies_pi : Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/ProofObjectsTest.v b/lf-current/ProofObjectsTest.v index 2a5a58221..2967460b0 100644 --- a/lf-current/ProofObjectsTest.v +++ b/lf-current/ProofObjectsTest.v @@ -345,4 +345,4 @@ idtac "---------- pe_implies_pi ---------". Print Assumptions pe_implies_pi. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Rel.html b/lf-current/Rel.html index b6fbe4db5..4eb6081ca 100644 --- a/lf-current/Rel.html +++ b/lf-current/Rel.html @@ -641,7 +641,7 @@

RelProperties of Relations -(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Rel.v b/lf-current/Rel.v index f258caa22..f3b1ba0f8 100644 --- a/lf-current/Rel.v +++ b/lf-current/Rel.v @@ -409,4 +409,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/RelTest.v b/lf-current/RelTest.v index 0d60781c4..e96428315 100644 --- a/lf-current/RelTest.v +++ b/lf-current/RelTest.v @@ -63,4 +63,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/Tactics.html b/lf-current/Tactics.html index d8804bafc..feea1b785 100644 --- a/lf-current/Tactics.html +++ b/lf-current/Tactics.html @@ -1849,7 +1849,7 @@

TacticsMore Basic Tactics

-(* 2024-07-10 18:39 *)
+(* 2024-08-08 20:33 *)
diff --git a/lf-current/Tactics.v b/lf-current/Tactics.v index 18ea910d6..c6867ed59 100644 --- a/lf-current/Tactics.v +++ b/lf-current/Tactics.v @@ -1242,4 +1242,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:33 *) diff --git a/lf-current/TacticsTest.v b/lf-current/TacticsTest.v index 170ea981a..fa702fc1f 100644 --- a/lf-current/TacticsTest.v +++ b/lf-current/TacticsTest.v @@ -254,4 +254,4 @@ idtac "---------- existsb_existsb' ---------". Print Assumptions existsb_existsb'. Abort. -(* 2024-07-10 18:39 *) +(* 2024-08-08 20:34 *) diff --git a/lf-current/index.html b/lf-current/index.html index 37548fe6a..9064995d0 100644 --- a/lf-current/index.html +++ b/lf-current/index.html @@ -73,7 +73,7 @@
Read

Download
-

Version 6.6 (2024-07-10 18:50, Coq 8.17.1 or later)

+

Version 6.6 (2024-08-08 20:43, Coq 8.17.1 or later)

diff --git a/lf-current/lf.tgz b/lf-current/lf.tgz index b4afe547f..aae545d15 100644 Binary files a/lf-current/lf.tgz and b/lf-current/lf.tgz differ diff --git a/plf-current/Bib.html b/plf-current/Bib.html index 62eb0d7d5..e7ead3ba0 100644 --- a/plf-current/Bib.html +++ b/plf-current/Bib.html @@ -94,7 +94,7 @@

BibBibliography

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Bib.v b/plf-current/Bib.v index 1456b42eb..206adbb30 100644 --- a/plf-current/Bib.v +++ b/plf-current/Bib.v @@ -39,4 +39,4 @@ (** $Date$ *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/BibTest.v b/plf-current/BibTest.v index 8c265e979..931d0af64 100644 --- a/plf-current/BibTest.v +++ b/plf-current/BibTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Equiv.html b/plf-current/Equiv.html index 1d65b2e2f..7ede2e978 100644 --- a/plf-current/Equiv.html +++ b/plf-current/Equiv.html @@ -2328,7 +2328,7 @@

EquivProgram Equivalence

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Equiv.v b/plf-current/Equiv.v index a26b3116a..554956481 100644 --- a/plf-current/Equiv.v +++ b/plf-current/Equiv.v @@ -1779,4 +1779,4 @@ Theorem zprop_preserving : forall c c', Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/EquivTest.v b/plf-current/EquivTest.v index fd76ef6fe..5289d4f18 100644 --- a/plf-current/EquivTest.v +++ b/plf-current/EquivTest.v @@ -293,4 +293,4 @@ idtac "---------- Himp.p3_p4_inequiv ---------". Print Assumptions Himp.p3_p4_inequiv. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Hoare.html b/plf-current/Hoare.html index aa14125fb..c7e0427e0 100644 --- a/plf-current/Hoare.html +++ b/plf-current/Hoare.html @@ -3178,7 +3178,7 @@

HoareHoare Logic, Part I

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Hoare.v b/plf-current/Hoare.v index 2b28a3ba6..f5794e10f 100644 --- a/plf-current/Hoare.v +++ b/plf-current/Hoare.v @@ -2330,4 +2330,4 @@ End HoareAssertAssume. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Hoare2.html b/plf-current/Hoare2.html index 54febd9af..4a62ab18c 100644 --- a/plf-current/Hoare2.html +++ b/plf-current/Hoare2.html @@ -2488,7 +2488,7 @@

Hoare2Hoare Logic, Part II -(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Hoare2.v b/plf-current/Hoare2.v index 4c2da0fd7..314508f88 100644 --- a/plf-current/Hoare2.v +++ b/plf-current/Hoare2.v @@ -2025,4 +2025,4 @@ Proof. End Himp2. (** [] *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Hoare2Test.v b/plf-current/Hoare2Test.v index 9f86c616e..d004afc05 100644 --- a/plf-current/Hoare2Test.v +++ b/plf-current/Hoare2Test.v @@ -132,4 +132,4 @@ idtac "---------- factorial_correct ---------". Print Assumptions factorial_correct. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/HoareAsLogic.html b/plf-current/HoareAsLogic.html index a9b6dd26e..e5bf24c29 100644 --- a/plf-current/HoareAsLogic.html +++ b/plf-current/HoareAsLogic.html @@ -570,7 +570,7 @@

HoareAsLogicHoare Logic as a Logic
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/HoareAsLogic.v b/plf-current/HoareAsLogic.v index cc2a45363..d95b26660 100644 --- a/plf-current/HoareAsLogic.v +++ b/plf-current/HoareAsLogic.v @@ -392,4 +392,4 @@ Proof. of Coq's logic. But this logic is far too powerful to be decidable. *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/HoareAsLogicTest.v b/plf-current/HoareAsLogicTest.v index 34a7efa29..e89d4f92e 100644 --- a/plf-current/HoareAsLogicTest.v +++ b/plf-current/HoareAsLogicTest.v @@ -160,4 +160,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/HoareTest.v b/plf-current/HoareTest.v index 844e13d84..3ee7de76e 100644 --- a/plf-current/HoareTest.v +++ b/plf-current/HoareTest.v @@ -371,4 +371,4 @@ idtac "---------- Himp.havoc_post ---------". Print Assumptions Himp.havoc_post. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Imp.v b/plf-current/Imp.v index 9038b25ed..3561df731 100644 --- a/plf-current/Imp.v +++ b/plf-current/Imp.v @@ -2077,4 +2077,4 @@ End BreakImp. [] *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/ImpTest.v b/plf-current/ImpTest.v index 84aa7a751..46723e16e 100644 --- a/plf-current/ImpTest.v +++ b/plf-current/ImpTest.v @@ -311,4 +311,4 @@ idtac "---------- BreakImp.seq_stops_on_break ---------". Print Assumptions BreakImp.seq_stops_on_break. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/LibTactics.html b/plf-current/LibTactics.html index bf7816821..120b0a8f2 100644 --- a/plf-current/LibTactics.html +++ b/plf-current/LibTactics.html @@ -5782,7 +5782,7 @@

LibTacticsA Collection of Handy Gene Open Scope nat_scope.

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/LibTactics.v b/plf-current/LibTactics.v index 503df955c..3bb61f372 100644 --- a/plf-current/LibTactics.v +++ b/plf-current/LibTactics.v @@ -4968,4 +4968,4 @@ End LibTacticsCompatibility. Open Scope nat_scope. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/LibTacticsTest.v b/plf-current/LibTacticsTest.v index 954263a7e..99ee0a8c5 100644 --- a/plf-current/LibTacticsTest.v +++ b/plf-current/LibTacticsTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Maps.v b/plf-current/Maps.v index c8f79ecd6..aa497804c 100644 --- a/plf-current/Maps.v +++ b/plf-current/Maps.v @@ -379,4 +379,4 @@ Qed. used to keep track of which program variables are defined in a given scope. *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/MapsTest.v b/plf-current/MapsTest.v index d868c4883..074e35b78 100644 --- a/plf-current/MapsTest.v +++ b/plf-current/MapsTest.v @@ -91,4 +91,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/MoreStlc.html b/plf-current/MoreStlc.html index 04f0ce24e..20836b7ab 100644 --- a/plf-current/MoreStlc.html +++ b/plf-current/MoreStlc.html @@ -2749,7 +2749,7 @@

MoreStlcMore on the Simply Typed Lam
End STLCExtended.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/MoreStlc.v b/plf-current/MoreStlc.v index 6fa24ded9..f90ad6f0b 100644 --- a/plf-current/MoreStlc.v +++ b/plf-current/MoreStlc.v @@ -2101,4 +2101,4 @@ Proof with eauto. End STLCExtended. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/MoreStlcTest.v b/plf-current/MoreStlcTest.v index d5e2dbc82..3ed40d61f 100644 --- a/plf-current/MoreStlcTest.v +++ b/plf-current/MoreStlcTest.v @@ -160,4 +160,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Norm.html b/plf-current/Norm.html index 69f7a7365..1d1469567 100644 --- a/plf-current/Norm.html +++ b/plf-current/Norm.html @@ -1467,7 +1467,7 @@

NormNormalization of STLC


-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Norm.v b/plf-current/Norm.v index d895bd1c6..3d1a009af 100644 --- a/plf-current/Norm.v +++ b/plf-current/Norm.v @@ -1144,4 +1144,4 @@ Proof. eapply V_nil. Qed. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/NormTest.v b/plf-current/NormTest.v index ae9c6bef1..cb5a1a20c 100644 --- a/plf-current/NormTest.v +++ b/plf-current/NormTest.v @@ -80,4 +80,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/PE.html b/plf-current/PE.html index b1f1e5846..130d1e949 100644 --- a/plf-current/PE.html +++ b/plf-current/PE.html @@ -1842,7 +1842,7 @@

PEPartial Evaluation

      destruct k as [k|]; inversion Hlookup; subst.
      eapply E_Some; eauto. apply pe_block_correct. apply Hkeval.
Qed.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/PE.v b/plf-current/PE.v index 9b7b20907..8defd1d14 100644 --- a/plf-current/PE.v +++ b/plf-current/PE.v @@ -1673,4 +1673,4 @@ Proof. intros. eapply E_Some; eauto. apply pe_block_correct. apply Hkeval. Qed. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/PETest.v b/plf-current/PETest.v index 3b02b7c13..af5b7d8f3 100644 --- a/plf-current/PETest.v +++ b/plf-current/PETest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Postscript.html b/plf-current/Postscript.html index 6330a7d75..68f2cc26f 100644 --- a/plf-current/Postscript.html +++ b/plf-current/Postscript.html @@ -550,7 +550,7 @@

Postscript

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Postscript.v b/plf-current/Postscript.v index 627131020..2b9007909 100644 --- a/plf-current/Postscript.v +++ b/plf-current/Postscript.v @@ -292,4 +292,4 @@ (** $Date$ *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/PostscriptTest.v b/plf-current/PostscriptTest.v index 57d4c3b92..148ec0061 100644 --- a/plf-current/PostscriptTest.v +++ b/plf-current/PostscriptTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Preface.html b/plf-current/Preface.html index 8919f494a..a366b9734 100644 --- a/plf-current/Preface.html +++ b/plf-current/Preface.html @@ -264,7 +264,7 @@

Preface

-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Preface.v b/plf-current/Preface.v index dd099b7fe..05d95e654 100644 --- a/plf-current/Preface.v +++ b/plf-current/Preface.v @@ -183,4 +183,4 @@ NSF Expeditions grant 1521523, _The Science of Deep Specification_. *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/PrefaceTest.v b/plf-current/PrefaceTest.v index bfefeb3f0..607e95063 100644 --- a/plf-current/PrefaceTest.v +++ b/plf-current/PrefaceTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/RecordSub.html b/plf-current/RecordSub.html index f3ffc0338..bd977063a 100644 --- a/plf-current/RecordSub.html +++ b/plf-current/RecordSub.html @@ -1179,7 +1179,7 @@

RecordSubSubtyping with Records End RecordSub.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/RecordSub.v b/plf-current/RecordSub.v index 72699405e..85dcebb1c 100644 --- a/plf-current/RecordSub.v +++ b/plf-current/RecordSub.v @@ -861,4 +861,4 @@ Proof with eauto. End RecordSub. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/RecordSubTest.v b/plf-current/RecordSubTest.v index 3a717045a..734fc4891 100644 --- a/plf-current/RecordSubTest.v +++ b/plf-current/RecordSubTest.v @@ -203,4 +203,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Records.html b/plf-current/Records.html index 6811802e9..a82c960f9 100644 --- a/plf-current/Records.html +++ b/plf-current/Records.html @@ -943,7 +943,7 @@

RecordsAdding Records to STLC     apply T_RCons... eapply step_preserves_record_tm...
Qed.
End STLCExtendedRecords.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Records.v b/plf-current/Records.v index 8d4982a76..f62bba41e 100644 --- a/plf-current/Records.v +++ b/plf-current/Records.v @@ -737,4 +737,4 @@ Qed. End STLCExtendedRecords. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/RecordsTest.v b/plf-current/RecordsTest.v index 7541da738..0aad53b61 100644 --- a/plf-current/RecordsTest.v +++ b/plf-current/RecordsTest.v @@ -149,4 +149,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/References.html b/plf-current/References.html index 56b8bc19d..9db13bea5 100644 --- a/plf-current/References.html +++ b/plf-current/References.html @@ -2657,7 +2657,7 @@

ReferencesTyping Mutable References< End RefsAndNontermination.
End STLCRef.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/References.v b/plf-current/References.v index 8f42e15f8..73e52e221 100644 --- a/plf-current/References.v +++ b/plf-current/References.v @@ -1947,4 +1947,4 @@ Qed. End RefsAndNontermination. End STLCRef. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/ReferencesTest.v b/plf-current/ReferencesTest.v index 593e709b7..610e301d2 100644 --- a/plf-current/ReferencesTest.v +++ b/plf-current/ReferencesTest.v @@ -158,4 +158,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Smallstep.html b/plf-current/Smallstep.html index fa10295ca..5f7368632 100644 --- a/plf-current/Smallstep.html +++ b/plf-current/Smallstep.html @@ -2668,7 +2668,7 @@

SmallstepSmall-step Operational Sema
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Smallstep.v b/plf-current/Smallstep.v index cbb07b784..e7017caa3 100644 --- a/plf-current/Smallstep.v +++ b/plf-current/Smallstep.v @@ -1909,4 +1909,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/SmallstepTest.v b/plf-current/SmallstepTest.v index 4cfc8576e..a3776ff20 100644 --- a/plf-current/SmallstepTest.v +++ b/plf-current/SmallstepTest.v @@ -252,4 +252,4 @@ idtac "---------- compiler_is_correct ---------". Print Assumptions compiler_is_correct. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Stlc.html b/plf-current/Stlc.html index 51ce19546..265b99a5a 100644 --- a/plf-current/Stlc.html +++ b/plf-current/Stlc.html @@ -1358,7 +1358,7 @@

StlcThe Simply Typed Lambda-Calculus
End STLC.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Stlc.v b/plf-current/Stlc.v index eb4602b7e..e9884feb5 100644 --- a/plf-current/Stlc.v +++ b/plf-current/Stlc.v @@ -912,4 +912,4 @@ Proof. End STLC. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/StlcProp.html b/plf-current/StlcProp.html index f37041d42..b5e0e2df3 100644 --- a/plf-current/StlcProp.html +++ b/plf-current/StlcProp.html @@ -1627,7 +1627,7 @@

StlcPropProperties of STLC End STLCArith.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/StlcProp.v b/plf-current/StlcProp.v index 1c1f986f0..8bd0c10a9 100644 --- a/plf-current/StlcProp.v +++ b/plf-current/StlcProp.v @@ -1036,4 +1036,4 @@ Proof with eauto. (* FILL IN HERE *) Admitted. End STLCArith. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/StlcPropTest.v b/plf-current/StlcPropTest.v index c1bf2fa68..f4962fffd 100644 --- a/plf-current/StlcPropTest.v +++ b/plf-current/StlcPropTest.v @@ -240,4 +240,4 @@ idtac "---------- STLCProp.substitution_preserves_typing_from_typing_ind ------- Print Assumptions STLCProp.substitution_preserves_typing_from_typing_ind. Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/StlcTest.v b/plf-current/StlcTest.v index 2580c6532..162b890ef 100644 --- a/plf-current/StlcTest.v +++ b/plf-current/StlcTest.v @@ -123,4 +123,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Sub.html b/plf-current/Sub.html index 90415540a..d0d67e222 100644 --- a/plf-current/Sub.html +++ b/plf-current/Sub.html @@ -2970,7 +2970,7 @@

SubSubtyping

End FormalThoughtExercises.
End STLCSub.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Sub.v b/plf-current/Sub.v index 49ea995f4..0e639ab18 100644 --- a/plf-current/Sub.v +++ b/plf-current/Sub.v @@ -1793,4 +1793,4 @@ End FormalThoughtExercises. End STLCSub. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/SubTest.v b/plf-current/SubTest.v index b4c5f73f1..3d2258067 100644 --- a/plf-current/SubTest.v +++ b/plf-current/SubTest.v @@ -230,4 +230,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Typechecking.html b/plf-current/Typechecking.html index 1a8fdd3a9..c884823ca 100644 --- a/plf-current/Typechecking.html +++ b/plf-current/Typechecking.html @@ -853,7 +853,7 @@

TypecheckingA Typechecker for STLC -(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Typechecking.v b/plf-current/Typechecking.v index 025bb1fe3..296fab401 100644 --- a/plf-current/Typechecking.v +++ b/plf-current/Typechecking.v @@ -685,4 +685,4 @@ Import StepFunction. End StlcImpl. (** [] *) -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/TypecheckingTest.v b/plf-current/TypecheckingTest.v index 22a69d366..abf74c667 100644 --- a/plf-current/TypecheckingTest.v +++ b/plf-current/TypecheckingTest.v @@ -106,4 +106,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/Types.html b/plf-current/Types.html index 0213e71d2..39a3783f1 100644 --- a/plf-current/Types.html +++ b/plf-current/Types.html @@ -1118,7 +1118,7 @@

TypesType Systems

End TM.
-(* 2024-07-10 18:40 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/Types.v b/plf-current/Types.v index f4caec44c..f42958fc7 100644 --- a/plf-current/Types.v +++ b/plf-current/Types.v @@ -705,4 +705,4 @@ Definition manual_grade_for_prog_pres_bigstep : option (nat*string) := None. (** [] *) End TM. -(* 2024-07-10 18:40 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/TypesTest.v b/plf-current/TypesTest.v index dcb0568f2..48b1fc9cb 100644 --- a/plf-current/TypesTest.v +++ b/plf-current/TypesTest.v @@ -218,4 +218,4 @@ idtac "---------- prog_pres_bigstep ---------". idtac "MANUAL". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/UseAuto.html b/plf-current/UseAuto.html index dc9b38c20..cd10a8a91 100644 --- a/plf-current/UseAuto.html +++ b/plf-current/UseAuto.html @@ -2491,7 +2491,7 @@

UseAutoTheory and Practice of Automa
-(* 2024-07-10 18:41 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/UseAuto.v b/plf-current/UseAuto.v index a47b3c475..70ac53b9b 100644 --- a/plf-current/UseAuto.v +++ b/plf-current/UseAuto.v @@ -1938,4 +1938,4 @@ Proof. congruence. Qed. some investment, however this investment will pay off very quickly. *) -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/UseAutoTest.v b/plf-current/UseAutoTest.v index 0ecb1d7d4..7289a0966 100644 --- a/plf-current/UseAutoTest.v +++ b/plf-current/UseAutoTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:36 *) diff --git a/plf-current/UseTactics.html b/plf-current/UseTactics.html index f33f64e38..1ee23d743 100644 --- a/plf-current/UseTactics.html +++ b/plf-current/UseTactics.html @@ -1256,7 +1256,7 @@

UseTactics: Tactic Library for CoqA
-(* 2024-07-10 18:41 *)
+(* 2024-08-08 20:35 *)
diff --git a/plf-current/UseTactics.v b/plf-current/UseTactics.v index 07e9ffd14..962c01d5b 100644 --- a/plf-current/UseTactics.v +++ b/plf-current/UseTactics.v @@ -920,4 +920,4 @@ End ExamplesLets. *) -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:35 *) diff --git a/plf-current/UseTacticsTest.v b/plf-current/UseTacticsTest.v index 87f59218c..2a3cddad3 100644 --- a/plf-current/UseTacticsTest.v +++ b/plf-current/UseTacticsTest.v @@ -60,4 +60,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:41 *) +(* 2024-08-08 20:36 *) diff --git a/plf-current/index.html b/plf-current/index.html index 62b9c44c7..22c7d6270 100644 --- a/plf-current/index.html +++ b/plf-current/index.html @@ -76,7 +76,7 @@
Download
-

Version 6.6 (2024-07-10 18:50, Coq 8.17.1 or later)

+

Version 6.6 (2024-08-08 20:43, Coq 8.17.1 or later)

diff --git a/plf-current/plf.tgz b/plf-current/plf.tgz index dd3bb518c..10e582fc4 100644 Binary files a/plf-current/plf.tgz and b/plf-current/plf.tgz differ diff --git a/qc-current/Bib.html b/qc-current/Bib.html index f9ecf4423..2f644e548 100644 --- a/qc-current/Bib.html +++ b/qc-current/Bib.html @@ -48,7 +48,7 @@

BibBibliography

-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:43 *)
diff --git a/qc-current/Bib.v b/qc-current/Bib.v index 8c82f62cf..508766936 100644 --- a/qc-current/Bib.v +++ b/qc-current/Bib.v @@ -9,4 +9,4 @@ ad-hoc Polymorphism Less ad-hoc_. POPL 1989. *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:43 *) diff --git a/qc-current/Introduction.html b/qc-current/Introduction.html index defa0d322..e604be0e3 100644 --- a/qc-current/Introduction.html +++ b/qc-current/Introduction.html @@ -207,7 +207,7 @@

Introduction

-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:42 *)
diff --git a/qc-current/Introduction.v b/qc-current/Introduction.v index ad1411693..c9e148063 100644 --- a/qc-current/Introduction.v +++ b/qc-current/Introduction.v @@ -124,4 +124,4 @@ Fixpoint insert x l := Finally, the [Postscript] chapter gives some suggestions for further reading. *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:42 *) diff --git a/qc-current/Postscript.html b/qc-current/Postscript.html index 96b6479c0..b00d02804 100644 --- a/qc-current/Postscript.html +++ b/qc-current/Postscript.html @@ -116,7 +116,7 @@

Postscript

-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:43 *)
diff --git a/qc-current/Postscript.v b/qc-current/Postscript.v index 4536ce63f..ea285165a 100644 --- a/qc-current/Postscript.v +++ b/qc-current/Postscript.v @@ -43,4 +43,4 @@ {https://lemonidas.github.io/pdf/Leo-PhD-Thesis.pdf} *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:43 *) diff --git a/qc-current/Preface.html b/qc-current/Preface.html index 56c2de3a0..ee3cbb7da 100644 --- a/qc-current/Preface.html +++ b/qc-current/Preface.html @@ -92,7 +92,7 @@

Preface

-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:42 *)
diff --git a/qc-current/Preface.v b/qc-current/Preface.v index 29a07efa4..5e40e5061 100644 --- a/qc-current/Preface.v +++ b/qc-current/Preface.v @@ -45,4 +45,4 @@ Specification_. Work on this volume was also supported by NSF grant 1421243, _Random Testing for Language Design_. *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:42 *) diff --git a/qc-current/QC.html b/qc-current/QC.html index cfcb529ef..cac803ef7 100644 --- a/qc-current/QC.html +++ b/qc-current/QC.html @@ -2289,7 +2289,7 @@

QCCore QuickChick

-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:42 *)
diff --git a/qc-current/QC.v b/qc-current/QC.v index b603e8f61..e6c065f35 100644 --- a/qc-current/QC.v +++ b/qc-current/QC.v @@ -1709,4 +1709,4 @@ Definition insertBST_spec' (low high : nat) (x : nat) (t : Tree nat) := [] *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:42 *) diff --git a/qc-current/QuickChickInterface.html b/qc-current/QuickChickInterface.html index b3d88889d..3c0a7f0a8 100644 --- a/qc-current/QuickChickInterface.html +++ b/qc-current/QuickChickInterface.html @@ -1012,7 +1012,7 @@

QuickChickInterfaceQuickChick Refere
End QuickChickSig.
-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:43 *)
diff --git a/qc-current/QuickChickInterface.v b/qc-current/QuickChickInterface.v index ddf8b9faf..b0f8d8c83 100644 --- a/qc-current/QuickChickInterface.v +++ b/qc-current/QuickChickInterface.v @@ -679,4 +679,4 @@ Record Args := End QuickChickSig. -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:43 *) diff --git a/qc-current/QuickChickTool.html b/qc-current/QuickChickTool.html index 0584eb343..af88b656f 100644 --- a/qc-current/QuickChickTool.html +++ b/qc-current/QuickChickTool.html @@ -659,7 +659,7 @@

QuickChickToolThe QuickChick Command
-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:43 *)
diff --git a/qc-current/QuickChickTool.v b/qc-current/QuickChickTool.v index 5eaf2e0ca..f6299336b 100644 --- a/qc-current/QuickChickTool.v +++ b/qc-current/QuickChickTool.v @@ -499,4 +499,4 @@ Definition compiles_correctly (e : exp) := (execute [] (compile e)) = [eval e]?. in [QuickChickInterface]. *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:43 *) diff --git a/qc-current/TImp.html b/qc-current/TImp.html index 2b1320e06..fc017c4a1 100644 --- a/qc-current/TImp.html +++ b/qc-current/TImp.html @@ -1852,7 +1852,7 @@

TImp: Case Studya Typed Imperative L
-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:42 *)
diff --git a/qc-current/TImp.v b/qc-current/TImp.v index 605ab9ff3..4db0f2be8 100644 --- a/qc-current/TImp.v +++ b/qc-current/TImp.v @@ -1410,4 +1410,4 @@ Conjecture conditional_prop_example : (** The first version of this material was developed in collaboration with Nicolas Koh. *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:42 *) diff --git a/qc-current/Typeclasses.html b/qc-current/Typeclasses.html index 3ed7cb532..eac4c11f7 100644 --- a/qc-current/Typeclasses.html +++ b/qc-current/Typeclasses.html @@ -2361,7 +2361,7 @@

TypeclassesA Tutorial on Typeclasses
-(* 2024-07-10 18:49 *)
+(* 2024-08-08 20:42 *)
diff --git a/qc-current/Typeclasses.v b/qc-current/Typeclasses.v index 659da6758..08e5593f2 100644 --- a/qc-current/Typeclasses.v +++ b/qc-current/Typeclasses.v @@ -1767,4 +1767,4 @@ Definition e4 : list nat := mymap false. {http://learnyouahaskell.com/making-our-own-types-and-typeclasses} *) -(* 2024-07-10 18:49 *) +(* 2024-08-08 20:42 *) diff --git a/qc-current/index.html b/qc-current/index.html index 1900f9ffd..aa9e7c70f 100644 --- a/qc-current/index.html +++ b/qc-current/index.html @@ -41,7 +41,7 @@
Read

Download
-

Version 1.3.3 (2024-07-10 18:51, Coq 8.17.1 or later)

+

Version 1.3.3 (2024-08-08 20:44, Coq 8.17.1 or later)

diff --git a/qc-current/qc.tgz b/qc-current/qc.tgz index 8c557aae7..199b943ca 100644 Binary files a/qc-current/qc.tgz and b/qc-current/qc.tgz differ diff --git a/slf-current/Affine.html b/slf-current/Affine.html index 529c4da23..6476d287d 100644 --- a/slf-current/Affine.html +++ b/slf-current/Affine.html @@ -1680,7 +1680,7 @@

AffineAffine Separation Logic
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Affine.v b/slf-current/Affine.v index a5debcbb1..de40f2552 100644 --- a/slf-current/Affine.v +++ b/slf-current/Affine.v @@ -1234,4 +1234,4 @@ End FromPreToPostGC. approach to controlling linearity was introduced in the context of CFML, in work by [Guéneau, Jourdan, Charguéraud, and Pottier 2019] (in Bib.v). *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Arrays.html b/slf-current/Arrays.html index b497ab804..fb0954712 100644 --- a/slf-current/Arrays.html +++ b/slf-current/Arrays.html @@ -1969,7 +1969,7 @@

ArraysReasoning about Arrays<
End Pivot.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Arrays.v b/slf-current/Arrays.v index 061561835..7225eaf2a 100644 --- a/slf-current/Arrays.v +++ b/slf-current/Arrays.v @@ -1548,4 +1548,4 @@ Qed. End Pivot. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Basic.html b/slf-current/Basic.html index bbf8c5e42..89a3dc7ba 100644 --- a/slf-current/Basic.html +++ b/slf-current/Basic.html @@ -2085,7 +2085,7 @@

BasicBasic Proofs in Separation Logi
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Basic.v b/slf-current/Basic.v index 9a3806bd1..7e87ce39c 100644 --- a/slf-current/Basic.v +++ b/slf-current/Basic.v @@ -1424,4 +1424,4 @@ Proof using. (* FILL IN HERE *) Admitted. predicates are directly inspired from those introduced in the Ynot project [Chlipala et al 2009] (in Bib.v). See chapter [Bib] for references. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Bib.html b/slf-current/Bib.html index a70b1cec7..163819140 100644 --- a/slf-current/Bib.html +++ b/slf-current/Bib.html @@ -275,7 +275,7 @@

BibBibliography

-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Bib.v b/slf-current/Bib.v index 691677401..92594665b 100644 --- a/slf-current/Bib.v +++ b/slf-current/Bib.v @@ -178,4 +178,4 @@ *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Himpl.html b/slf-current/Himpl.html index c6a4498e0..0ad1483e8 100644 --- a/slf-current/Himpl.html +++ b/slf-current/Himpl.html @@ -1199,7 +1199,7 @@

HimplHeap Entailment

-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Himpl.v b/slf-current/Himpl.v index 1f5b9f895..8bebb084b 100644 --- a/slf-current/Himpl.v +++ b/slf-current/Himpl.v @@ -875,4 +875,4 @@ End EntailmentRulesProofs. (* ================================================================= *) (** ** Historical Notes *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Hprop.html b/slf-current/Hprop.html index 432ff359f..aa260d8dd 100644 --- a/slf-current/Hprop.html +++ b/slf-current/Hprop.html @@ -988,7 +988,7 @@

HpropHeap Predicates

-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Hprop.v b/slf-current/Hprop.v index db5be9218..c3adf9dab 100644 --- a/slf-current/Hprop.v +++ b/slf-current/Hprop.v @@ -680,4 +680,4 @@ End Extensionality. had spotted the potential benefit of working with the separating conjunction. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibAxioms.v b/slf-current/LibAxioms.v index 3a12f8fb9..671d5903a 100644 --- a/slf-current/LibAxioms.v +++ b/slf-current/LibAxioms.v @@ -52,4 +52,4 @@ Axiom indefinite_description : forall (A : Type) (P : A->Prop), ex P -> sig P. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibBool.v b/slf-current/LibBool.v index 835c9bc94..f94369a7b 100644 --- a/slf-current/LibBool.v +++ b/slf-current/LibBool.v @@ -387,4 +387,4 @@ Tactic Notation "rew_bool" "~" "in" "*" := Tactic Notation "rew_bool" "*" "in" "*" := rew_bool in *; auto_star. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibChoice.v b/slf-current/LibChoice.v index 4cf978fa7..16c4477ea 100644 --- a/slf-current/LibChoice.v +++ b/slf-current/LibChoice.v @@ -215,4 +215,4 @@ Proof using. intros. apply~ guarded_rel_choice. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibContainer.v b/slf-current/LibContainer.v index e297cb21f..eeeb8c8b2 100644 --- a/slf-current/LibContainer.v +++ b/slf-current/LibContainer.v @@ -970,4 +970,4 @@ Qed. End DerivedProperties. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibCore.v b/slf-current/LibCore.v index fed54dab0..1f5af7dfa 100644 --- a/slf-current/LibCore.v +++ b/slf-current/LibCore.v @@ -16,4 +16,4 @@ Open Scope Z_scope. Open Scope Int_scope. Open Scope comp_scope. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibEpsilon.v b/slf-current/LibEpsilon.v index 466f0575e..a9797c85b 100644 --- a/slf-current/LibEpsilon.v +++ b/slf-current/LibEpsilon.v @@ -233,4 +233,4 @@ End Rel_to_fun. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibEqual.v b/slf-current/LibEqual.v index 93d34ee82..7b7385391 100644 --- a/slf-current/LibEqual.v +++ b/slf-current/LibEqual.v @@ -922,4 +922,4 @@ Proof using. apply~ eq_dep_of_JMeq. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibFun.v b/slf-current/LibFun.v index 72a17484e..22e36146d 100644 --- a/slf-current/LibFun.v +++ b/slf-current/LibFun.v @@ -260,4 +260,4 @@ Proof using. introv I. induction n; introv Hx; autos*. Qed. (* --TODO: rename applyn to iter *) (* --TODO: migrate iteration of functionals from LibFix to here *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibInt.v b/slf-current/LibInt.v index f596618a2..1b122e3b6 100644 --- a/slf-current/LibInt.v +++ b/slf-current/LibInt.v @@ -925,4 +925,4 @@ Tactic Notation "rew_to_nat_nonneg" := Tactic Notation "rew_to_nat_nonneg" "~" := autorewrite with rew_to_nat_nonneg; try math; autos~. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibList.v b/slf-current/LibList.v index 7b219661f..5cdb7a916 100644 --- a/slf-current/LibList.v +++ b/slf-current/LibList.v @@ -3981,4 +3981,4 @@ Tactic Notation "list2_ind_last" constr(E) := match type of E with length ?l1 = length ?l2 => list2_ind_last l1 l2; [ apply E | | ] end. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibListExec.v b/slf-current/LibListExec.v index 36bc3008a..190ddedfa 100644 --- a/slf-current/LibListExec.v +++ b/slf-current/LibListExec.v @@ -328,4 +328,4 @@ Proof using. extens. intros a b l. induction l; simpl; rew_listx; fequals. Qed. #[global] Hint Rewrite fold_right_eq : rew_list_exec. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibListZ.v b/slf-current/LibListZ.v index f3c762b5a..2a78faa8f 100644 --- a/slf-current/LibListZ.v +++ b/slf-current/LibListZ.v @@ -1510,4 +1510,4 @@ Qed. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibLogic.v b/slf-current/LibLogic.v index 14aa8794a..c9ba6382f 100644 --- a/slf-current/LibLogic.v +++ b/slf-current/LibLogic.v @@ -1183,4 +1183,4 @@ Arguments forall_conj_inv_10 [A1] [A2] [A3] [A4] [A5] [A6] [A7] [A8] [A9] [A10] Arguments forall_conj_inv_11 [A1] [A2] [A3] [A4] [A5] [A6] [A7] [A8] [A9] [A10] [A11] [P] [Q]. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibMin.v b/slf-current/LibMin.v index 098469a25..1481e044a 100644 --- a/slf-current/LibMin.v +++ b/slf-current/LibMin.v @@ -258,4 +258,4 @@ Definition MMax `{Inhab A} `{Le A} := mmax le. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibMonoid.v b/slf-current/LibMonoid.v index 57215911b..e9f42a0a3 100644 --- a/slf-current/LibMonoid.v +++ b/slf-current/LibMonoid.v @@ -122,4 +122,4 @@ Qed. End MonoidInst. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibMultiset.v b/slf-current/LibMultiset.v index 5d12d3de3..fafeae27c 100644 --- a/slf-current/LibMultiset.v +++ b/slf-current/LibMultiset.v @@ -754,4 +754,4 @@ Tactic Notation "multiset_empty" := Tactic Notation "multiset_empty" constr(E) := let H := fresh "M" in lets H:E; multiset_empty in H. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibNat.v b/slf-current/LibNat.v index 72a01b091..a10e75510 100644 --- a/slf-current/LibNat.v +++ b/slf-current/LibNat.v @@ -282,4 +282,4 @@ Proof using. rewrite IHn1. extens. rew_istrue. nat_math. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibOperation.v b/slf-current/LibOperation.v index b21373f76..1355d0897 100644 --- a/slf-current/LibOperation.v +++ b/slf-current/LibOperation.v @@ -212,4 +212,4 @@ Qed. End OpProperties. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibOption.v b/slf-current/LibOption.v index 6f422a75b..1f830d678 100644 --- a/slf-current/LibOption.v +++ b/slf-current/LibOption.v @@ -168,4 +168,4 @@ Arguments apply_on_eq_some_inv [A] [B] [f] [o] [x]. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibOrder.v b/slf-current/LibOrder.v index 978f3ac2e..543f51dbc 100644 --- a/slf-current/LibOrder.v +++ b/slf-current/LibOrder.v @@ -1167,4 +1167,4 @@ Lemma max_r : forall `{Le A} (n m:A), max n m = m. Proof using. introv T M. unfold max. case_if*. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibProd.v b/slf-current/LibProd.v index 0ef66a7d2..cb3df69f0 100644 --- a/slf-current/LibProd.v +++ b/slf-current/LibProd.v @@ -293,4 +293,4 @@ Tactic Notation "unfolds_unproj" := unproj41, unproj42, unproj43, unproj44, unproj51 in *. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibReflect.v b/slf-current/LibReflect.v index 11a8f5654..4cafe3a79 100644 --- a/slf-current/LibReflect.v +++ b/slf-current/LibReflect.v @@ -478,4 +478,4 @@ Ltac apply_to_head_of E cont ::= | ?A => go A end. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibRelation.v b/slf-current/LibRelation.v index 878ab0af2..e8784c8fe 100644 --- a/slf-current/LibRelation.v +++ b/slf-current/LibRelation.v @@ -2439,4 +2439,4 @@ Qed. End Rel_in_fun. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepFmap.html b/slf-current/LibSepFmap.html index d5c6d2cc3..e932d0301 100644 --- a/slf-current/LibSepFmap.html +++ b/slf-current/LibSepFmap.html @@ -1385,7 +1385,7 @@

LibSepFmapAppendix - Finite Mapsrewrite N in M1. false*.
Qed.
End FmapFresh.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/LibSepFmap.v b/slf-current/LibSepFmap.v index 6b570ba93..f1f0fe9d8 100644 --- a/slf-current/LibSepFmap.v +++ b/slf-current/LibSepFmap.v @@ -1199,4 +1199,4 @@ Qed. End FmapFresh. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepMinimal.html b/slf-current/LibSepMinimal.html index 5fa6f9856..d57b43c4c 100644 --- a/slf-current/LibSepMinimal.html +++ b/slf-current/LibSepMinimal.html @@ -884,7 +884,7 @@

LibSepMinimalAppendix - Minimalistic   intros m'. simpl. apply triple_hpure. intros →.
  { apply triple_set. }
Qed.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/LibSepMinimal.v b/slf-current/LibSepMinimal.v index 4c51c6424..0f145b050 100644 --- a/slf-current/LibSepMinimal.v +++ b/slf-current/LibSepMinimal.v @@ -718,4 +718,4 @@ Proof using. { apply triple_set. } Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepReference.html b/slf-current/LibSepReference.html index 9804ea5a1..963cbdada 100644 --- a/slf-current/LibSepReference.html +++ b/slf-current/LibSepReference.html @@ -4831,7 +4831,7 @@

LibSepReferenceAppendix - The Full C     (fun _ ⇒ \[]).
Proof using. xwp. xif; auto_false. intros _. xval. xsimpl. Qed.
End DemoPrograms.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/LibSepReference.v b/slf-current/LibSepReference.v index 6c5dcd1d0..f80a10825 100644 --- a/slf-current/LibSepReference.v +++ b/slf-current/LibSepReference.v @@ -4288,4 +4288,4 @@ Proof using. xwp. xif; auto_false. intros _. xval. xsimpl. Qed. End DemoPrograms. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepSimpl.html b/slf-current/LibSepSimpl.html index 326b42949..fd831a489 100644 --- a/slf-current/LibSepSimpl.html +++ b/slf-current/LibSepSimpl.html @@ -2152,7 +2152,7 @@

LibSepSimplAppendix - Simplification   intros. xchange (>> hforall_specialize 2). xsimpl.
Qed.
End XsimplSetup.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/LibSepSimpl.v b/slf-current/LibSepSimpl.v index 751ac2b87..5bb1db1bd 100644 --- a/slf-current/LibSepSimpl.v +++ b/slf-current/LibSepSimpl.v @@ -2026,4 +2026,4 @@ Qed. End XsimplSetup. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepTLCbuffer.v b/slf-current/LibSepTLCbuffer.v index 692bc58c8..a6f7ba541 100644 --- a/slf-current/LibSepTLCbuffer.v +++ b/slf-current/LibSepTLCbuffer.v @@ -22,4 +22,4 @@ Global Opaque Z.add. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSepVar.html b/slf-current/LibSepVar.html index 23eea341c..aaa925256 100644 --- a/slf-current/LibSepVar.html +++ b/slf-current/LibSepVar.html @@ -520,7 +520,7 @@

LibSepVarAppendix - Program Variable               [ false | apply E ] ] end.
#[global]
Hint Extern 1 (?x ≠ ?y) ⇒ var_neq.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/LibSepVar.v b/slf-current/LibSepVar.v index 566047840..5e922548f 100644 --- a/slf-current/LibSepVar.v +++ b/slf-current/LibSepVar.v @@ -437,4 +437,4 @@ Ltac var_neq := #[global] Hint Extern 1 (?x <> ?y) => var_neq. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSet.v b/slf-current/LibSet.v index c931bfd47..156fa773f 100644 --- a/slf-current/LibSet.v +++ b/slf-current/LibSet.v @@ -1143,4 +1143,4 @@ Tactic Notation "rew_foreach" "*" "in" "*" := *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibString.v b/slf-current/LibString.v index 422d505d3..41c9f3221 100644 --- a/slf-current/LibString.v +++ b/slf-current/LibString.v @@ -19,4 +19,4 @@ Require Export Coq.Strings.String. Instance Inhab_string : Inhab string. Proof using. apply (Inhab_of_val EmptyString). Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibSum.v b/slf-current/LibSum.v index 4c127ed9c..f8a2e0589 100644 --- a/slf-current/LibSum.v +++ b/slf-current/LibSum.v @@ -123,4 +123,4 @@ Definition fun_get22 f := End Fget. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibTactics.v b/slf-current/LibTactics.v index 9accb8be4..493644d87 100644 --- a/slf-current/LibTactics.v +++ b/slf-current/LibTactics.v @@ -5272,4 +5272,4 @@ Ltac autorewrite_in_star_patch cont := (* End of experimental features *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibUnit.v b/slf-current/LibUnit.v index e26a5e516..440e3bd93 100644 --- a/slf-current/LibUnit.v +++ b/slf-current/LibUnit.v @@ -49,4 +49,4 @@ Proof using. intros. destruct tt1. destruct~ tt2. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/LibWf.v b/slf-current/LibWf.v index 8bbc25b2f..b24d6a5c4 100644 --- a/slf-current/LibWf.v +++ b/slf-current/LibWf.v @@ -596,4 +596,4 @@ Proof using. induction 1; eauto using Acc_inv. Qed. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Postscript.html b/slf-current/Postscript.html index f5c94a44e..b78dffa7d 100644 --- a/slf-current/Postscript.html +++ b/slf-current/Postscript.html @@ -257,7 +257,7 @@

PostscriptConclusion and Perspective
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Postscript.v b/slf-current/Postscript.v index d733673da..4fbe653e8 100644 --- a/slf-current/Postscript.v +++ b/slf-current/Postscript.v @@ -117,4 +117,4 @@ *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Preface.html b/slf-current/Preface.html index 486fa344c..622786570 100644 --- a/slf-current/Preface.html +++ b/slf-current/Preface.html @@ -528,7 +528,7 @@

PrefaceIntroduction to the Course
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Preface.v b/slf-current/Preface.v index 87daee44d..bc558df20 100644 --- a/slf-current/Preface.v +++ b/slf-current/Preface.v @@ -294,4 +294,4 @@ Foundation under the NSF Expeditions grant 1521523, _The Science of Deep Specification_. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Records.html b/slf-current/Records.html index e1aea433f..e07bf937c 100644 --- a/slf-current/Records.html +++ b/slf-current/Records.html @@ -1027,7 +1027,7 @@

RecordsReasoning about Records
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Records.v b/slf-current/Records.v index 9292ccb56..2e5bfacb8 100644 --- a/slf-current/Records.v +++ b/slf-current/Records.v @@ -770,4 +770,4 @@ Ltac xapp_nosubst_for_records tt ::= (** The above definition is the one used in [LibSepReference]. It was put to practice in the chapters [Basic] and [Repr]. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Repr.html b/slf-current/Repr.html index 57da9006d..8cd856d46 100644 --- a/slf-current/Repr.html +++ b/slf-current/Repr.html @@ -2171,7 +2171,7 @@

ReprRepresentation Predicates
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Repr.v b/slf-current/Repr.v index 27ff0db53..2d22b07ec 100644 --- a/slf-current/Repr.v +++ b/slf-current/Repr.v @@ -1616,4 +1616,4 @@ Proof using. (* FILL IN HERE *) Admitted. history of higher-order Separation Logic for higher-order programs may be found in the companion course notes, linked in the [Preface]. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Rules.html b/slf-current/Rules.html index 6ae3f0d64..671553a21 100644 --- a/slf-current/Rules.html +++ b/slf-current/Rules.html @@ -1534,7 +1534,7 @@

RulesReasoning Rules for Term Constr
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Rules.v b/slf-current/Rules.v index b8af71598..fdfe51bfb 100644 --- a/slf-current/Rules.v +++ b/slf-current/Rules.v @@ -1007,4 +1007,4 @@ End ExamplePrograms2. (Isabelle/HOL, Coq, PVS, HOL4, HOL). For a detailed list, see the last chapter of the companion notes, linked from the [Preface]. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Triples.html b/slf-current/Triples.html index 9857b65b8..e27c0e8a8 100644 --- a/slf-current/Triples.html +++ b/slf-current/Triples.html @@ -2087,7 +2087,7 @@

TriplesStructural Reasoning Rules
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Triples.v b/slf-current/Triples.v index 5c2266966..baadf4a0c 100644 --- a/slf-current/Triples.v +++ b/slf-current/Triples.v @@ -1545,4 +1545,4 @@ End BakedInFrame. technique has been employed successfully in numerous formalizations of Separation Logic. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/WPgen.html b/slf-current/WPgen.html index f94b3077e..e354fcb66 100644 --- a/slf-current/WPgen.html +++ b/slf-current/WPgen.html @@ -3147,7 +3147,7 @@

WPgenWeakest Precondition Generator<
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/WPgen.v b/slf-current/WPgen.v index f18c5e732..4e01b99e0 100644 --- a/slf-current/WPgen.v +++ b/slf-current/WPgen.v @@ -2397,4 +2397,4 @@ End WPgenRec. the existence of a _pretty_ Separation Logic proof featuring local reasoning --that is, allowing for maximal usage of the frame rule. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/WPsem.html b/slf-current/WPsem.html index 2e2aec071..248b0ccd3 100644 --- a/slf-current/WPsem.html +++ b/slf-current/WPsem.html @@ -1242,7 +1242,7 @@

WPsemSemantics of Weakest Preconditi
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/WPsem.v b/slf-current/WPsem.v index 74fa7aafd..3baec902b 100644 --- a/slf-current/WPsem.v +++ b/slf-current/WPsem.v @@ -870,4 +870,4 @@ End TexanTriples. VST have advocated for this rule. The ramified frame rule was integrated in CFML 2.0 in 2018. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/WPsound.html b/slf-current/WPsound.html index 879a82ddb..07450bc54 100644 --- a/slf-current/WPsound.html +++ b/slf-current/WPsound.html @@ -776,7 +776,7 @@

WPsoundSoundness of the Weakest Prec     do 2 rewrite lookup_rem in K1. case_var. }
Qed.
End IsubstProp.
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/WPsound.v b/slf-current/WPsound.v index c8e193f57..1f1fd6dfe 100644 --- a/slf-current/WPsound.v +++ b/slf-current/WPsound.v @@ -588,4 +588,4 @@ Qed. End IsubstProp. -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/Wand.html b/slf-current/Wand.html index a612e7fe4..818910b56 100644 --- a/slf-current/Wand.html +++ b/slf-current/Wand.html @@ -1746,7 +1746,7 @@

WandThe Magic Wand and Other Operato
-(* 2024-07-10 18:43 *)
+(* 2024-08-08 20:37 *)
diff --git a/slf-current/Wand.v b/slf-current/Wand.v index bca76bb39..55f49ae2b 100644 --- a/slf-current/Wand.v +++ b/slf-current/Wand.v @@ -1273,4 +1273,4 @@ End QwandEquiv. [Hobor and Villard 2013] (in Bib.v). The rule has later been popularized by the Iris framework, in particular. *) -(* 2024-07-10 18:43 *) +(* 2024-08-08 20:37 *) diff --git a/slf-current/index.html b/slf-current/index.html index 915ebb4ad..423f955eb 100644 --- a/slf-current/index.html +++ b/slf-current/index.html @@ -43,7 +43,7 @@
Download
-

Version 2.1 (2024-07-10 18:50, Coq 8.17.1 or later)

+

Version 2.1 (2024-08-08 20:43, Coq 8.17.1 or later)

diff --git a/slf-current/slf.tgz b/slf-current/slf.tgz index cc9d07ed6..d5b287f88 100644 Binary files a/slf-current/slf.tgz and b/slf-current/slf.tgz differ diff --git a/vc-current/Bib.html b/vc-current/Bib.html index de06cec8e..a8f3df938 100644 --- a/vc-current/Bib.html +++ b/vc-current/Bib.html @@ -158,7 +158,7 @@

BibBibliography

-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Bib.v b/vc-current/Bib.v index 544d49e7e..acdec2c2f 100644 --- a/vc-current/Bib.v +++ b/vc-current/Bib.v @@ -89,4 +89,4 @@ *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Hashfun.html b/vc-current/Hashfun.html index 11c1b32fc..d3d3ca6c9 100644 --- a/vc-current/Hashfun.html +++ b/vc-current/Hashfun.html @@ -406,7 +406,7 @@

HashfunFunctional model of hash tabl
End IntHashTable.
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Hashfun.v b/vc-current/Hashfun.v index c47529fd1..e40b78e34 100644 --- a/vc-current/Hashfun.v +++ b/vc-current/Hashfun.v @@ -328,4 +328,4 @@ Proof. End IntHashTable. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Postscript.html b/vc-current/Postscript.html index af212022d..ca8bbacf1 100644 --- a/vc-current/Postscript.html +++ b/vc-current/Postscript.html @@ -265,7 +265,7 @@

PostscriptPostcript and bibliography
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Postscript.v b/vc-current/Postscript.v index 03ae8f811..e9ef82fd2 100644 --- a/vc-current/Postscript.v +++ b/vc-current/Postscript.v @@ -165,4 +165,4 @@ future software verification efforts. *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Preface.html b/vc-current/Preface.html index 2985fd25e..17a74a0a6 100644 --- a/vc-current/Preface.html +++ b/vc-current/Preface.html @@ -328,7 +328,7 @@

Preface

to install the properly configured clightgen outputs."
"It is not necessary to have clightgen installed".
Abort.
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Preface.v b/vc-current/Preface.v index 7a583d02b..0b81f0954 100644 --- a/vc-current/Preface.v +++ b/vc-current/Preface.v @@ -209,4 +209,4 @@ to install the properly configured clightgen outputs." "It is not necessary to have clightgen installed". Abort. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Spec_stack.html b/vc-current/Spec_stack.html index fadad92f9..2933c07a5 100644 --- a/vc-current/Spec_stack.html +++ b/vc-current/Spec_stack.html @@ -242,7 +242,7 @@

Spec_stackVSU specification of the S
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Spec_stack.v b/vc-current/Spec_stack.v index 3a0a04aa5..c60a2a92b 100644 --- a/vc-current/Spec_stack.v +++ b/vc-current/Spec_stack.v @@ -153,4 +153,4 @@ Check StackASI. (* : MallocFreeAPD -> StackAPD -> funspecs *) (* ================================================================= *) (** ** Next Chapter: [Spec_triang] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Spec_stdlib.html b/vc-current/Spec_stdlib.html index 80f307bb3..58d1082d1 100644 --- a/vc-current/Spec_stdlib.html +++ b/vc-current/Spec_stdlib.html @@ -337,7 +337,7 @@

Spec_stdlibSpecification of external
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Spec_stdlib.v b/vc-current/Spec_stdlib.v index 70d76f296..32942d6ac 100644 --- a/vc-current/Spec_stdlib.v +++ b/vc-current/Spec_stdlib.v @@ -256,4 +256,4 @@ Qed. (* ================================================================= *) (** ** Next Chapter: [VSU_stack] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Spec_triang.html b/vc-current/Spec_triang.html index 26cba59ac..9e8d48635 100644 --- a/vc-current/Spec_triang.html +++ b/vc-current/Spec_triang.html @@ -235,7 +235,7 @@

Spec_triangVSU specification of the
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Spec_triang.v b/vc-current/Spec_triang.v index e9adf62c6..c1ead4cfa 100644 --- a/vc-current/Spec_triang.v +++ b/vc-current/Spec_triang.v @@ -147,4 +147,4 @@ Check TriangASI. (* : MallocFreeAPD -> funspecs *) (* ================================================================= *) (** ** Next Chapter: [Spec_stdlib] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_intro.html b/vc-current/VSU_intro.html index e01469030..5b7190592 100644 --- a/vc-current/VSU_intro.html +++ b/vc-current/VSU_intro.html @@ -202,7 +202,7 @@

VSU_introIntroduction to Verified So
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_intro.v b/vc-current/VSU_intro.v index c935a22c6..5956a6dc4 100644 --- a/vc-current/VSU_intro.v +++ b/vc-current/VSU_intro.v @@ -111,4 +111,4 @@ (* ================================================================= *) (** ** Next Chapter: [Spec_stack] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_main.html b/vc-current/VSU_main.html index 81ce0c876..b291acdd9 100644 --- a/vc-current/VSU_main.html +++ b/vc-current/VSU_main.html @@ -598,7 +598,7 @@

VSU_mainlinking all the VSUs togethe
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_main.v b/vc-current/VSU_main.v index 613a65f96..d86c34c96 100644 --- a/vc-current/VSU_main.v +++ b/vc-current/VSU_main.v @@ -348,4 +348,4 @@ Eval red in (WholeProgSafeType WholeComp tt). (* ================================================================= *) (** ** Next Chapter: [VSU_stdlib2] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_main2.html b/vc-current/VSU_main2.html index e9c3130d8..0559fb40d 100644 --- a/vc-current/VSU_main2.html +++ b/vc-current/VSU_main2.html @@ -215,7 +215,7 @@

VSU_main2linking with stdlib2 instea Lemma WholeProgSafe: WholeProgSafeType WholeComp tt.
Proof. proveWholeProgSafe. Qed.
Eval red in WholeProgSafeType WholeComp tt.
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_main2.v b/vc-current/VSU_main2.v index 3c409fba3..f6cbf6e82 100644 --- a/vc-current/VSU_main2.v +++ b/vc-current/VSU_main2.v @@ -142,4 +142,4 @@ Proof. proveWholeProgSafe. Qed. Eval red in WholeProgSafeType WholeComp tt. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_stack.html b/vc-current/VSU_stack.html index 97a793601..005706847 100644 --- a/vc-current/VSU_stack.html +++ b/vc-current/VSU_stack.html @@ -412,7 +412,7 @@

VSU_stackVSU verification of the Sta
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_stack.v b/vc-current/VSU_stack.v index befad2604..47d3e712b 100644 --- a/vc-current/VSU_stack.v +++ b/vc-current/VSU_stack.v @@ -282,4 +282,4 @@ End Stack_VSU. (* ================================================================= *) (** ** Next Chapter: [VSU_triang] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_stdlib.html b/vc-current/VSU_stdlib.html index e34ded8f7..186f066bd 100644 --- a/vc-current/VSU_stdlib.html +++ b/vc-current/VSU_stdlib.html @@ -194,7 +194,7 @@

VSU_stdlibAxiomatization of malloc/f
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_stdlib.v b/vc-current/VSU_stdlib.v index c967c066d..bebfbe9f7 100644 --- a/vc-current/VSU_stdlib.v +++ b/vc-current/VSU_stdlib.v @@ -130,4 +130,4 @@ Qed. (* ================================================================= *) (** ** Next Chapter: [VSU_main] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_stdlib2.html b/vc-current/VSU_stdlib2.html index 9e6be369c..14915f079 100644 --- a/vc-current/VSU_stdlib2.html +++ b/vc-current/VSU_stdlib2.html @@ -455,7 +455,7 @@

VSU_stdlib2Malloc/free/exit programm
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_stdlib2.v b/vc-current/VSU_stdlib2.v index 86590b849..f34392acf 100644 --- a/vc-current/VSU_stdlib2.v +++ b/vc-current/VSU_stdlib2.v @@ -300,4 +300,4 @@ Qed. (* ================================================================= *) (** ** Next Chapter: [VSU_main2] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/VSU_triang.html b/vc-current/VSU_triang.html index cfc2ad8cb..9b43afd85 100644 --- a/vc-current/VSU_triang.html +++ b/vc-current/VSU_triang.html @@ -248,7 +248,7 @@

VSU_triangVSU verification of the Tr
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/VSU_triang.v b/vc-current/VSU_triang.v index f293da680..07bc9c534 100644 --- a/vc-current/VSU_triang.v +++ b/vc-current/VSU_triang.v @@ -141,4 +141,4 @@ End Triang_VSU. (* ================================================================= *) (** ** Next Chapter: [VSU_stdlib] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_append1.html b/vc-current/Verif_append1.html index 0c7b9dd1b..3087885a5 100644 --- a/vc-current/Verif_append1.html +++ b/vc-current/Verif_append1.html @@ -749,7 +749,7 @@

Verif_append1List segments -(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_append1.v b/vc-current/Verif_append1.v index a7cac7baa..1dee3736a 100644 --- a/vc-current/Verif_append1.v +++ b/vc-current/Verif_append1.v @@ -491,4 +491,4 @@ forward_if. (* if (x == NULL) *) (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_append2.html b/vc-current/Verif_append2.html index c4d608aaa..b874aea99 100644 --- a/vc-current/Verif_append2.html +++ b/vc-current/Verif_append2.html @@ -740,7 +740,7 @@

Verif_append2Magic wand, partial dat     sep_apply (data_at_conflict Tsh t_list (default_val t_list) (v, u) y); auto.
    entailer!.
Qed.
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_append2.v b/vc-current/Verif_append2.v index 2c11f5d28..0c182e2a4 100644 --- a/vc-current/Verif_append2.v +++ b/vc-current/Verif_append2.v @@ -493,4 +493,4 @@ Proof. entailer!. Qed. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_hash.html b/vc-current/Verif_hash.html index 8c42a28e5..655b11083 100644 --- a/vc-current/Verif_hash.html +++ b/vc-current/Verif_hash.html @@ -1592,7 +1592,7 @@

Verif_hashCorrectness proof of hash.
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_hash.v b/vc-current/Verif_hash.v index ada1cebe8..1ab727177 100644 --- a/vc-current/Verif_hash.v +++ b/vc-current/Verif_hash.v @@ -1140,4 +1140,4 @@ erewrite (wand_slice_array h (h+1) N _ (tptr tcell)) (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_reverse.html b/vc-current/Verif_reverse.html index b72f22ff4..63fc997c8 100644 --- a/vc-current/Verif_reverse.html +++ b/vc-current/Verif_reverse.html @@ -1181,7 +1181,7 @@

Verif_reverseLinked lists in Verifia
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_reverse.v b/vc-current/Verif_reverse.v index b5483f7ec..cd68eaea8 100644 --- a/vc-current/Verif_reverse.v +++ b/vc-current/Verif_reverse.v @@ -743,4 +743,4 @@ Abort. Separation logic is essential for reasoning about updates to these structures. Verifiable C's SEP clause ensures separation between all its conjuncts. *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_stack.html b/vc-current/Verif_stack.html index 2445d81c9..69282b5b9 100644 --- a/vc-current/Verif_stack.html +++ b/vc-current/Verif_stack.html @@ -442,7 +442,7 @@

Verif_stackStack ADT implemented by
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_stack.v b/vc-current/Verif_stack.v index cd35a89a3..f586e0724 100644 --- a/vc-current/Verif_stack.v +++ b/vc-current/Verif_stack.v @@ -303,4 +303,4 @@ start_function. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_strlib.html b/vc-current/Verif_strlib.html index cf9217fd9..014df984d 100644 --- a/vc-current/Verif_strlib.html +++ b/vc-current/Verif_strlib.html @@ -655,7 +655,7 @@

Verif_strlibString functions< Check upd_Znth_app1. (* Hint: this lemma will be useful. *)
Check app_Znth2. (* Hint: this lemma will be useful. *)
Check Znth_0_cons. (* Hint: this lemma will be useful. *)
-(* Other useful lemmas will be map_app, app_ass *)
+(* Other useful lemmas will be map_app, app_assoc *)
(* FILL IN HERE *) Admitted.
☐ @@ -687,7 +687,7 @@

Verif_strlibString functions<
Useful lemmas here will be: upd_Znth_app2, sublist_split, -repeat_app', app_Znth1, map_app, app_ass, sublist_len_1. +repeat_app', app_Znth1, map_app, app_assoc, sublist_len_1.
(* FILL IN HERE *) Admitted.
@@ -732,7 +732,7 @@

Verif_strlibString functions< rewrite <- Zrepeat_app by lia.
replace (n-i) with (1 + (n-(i+1))) by lia.
rewrite <- Zrepeat_app by lia.
-rewrite !app_ass.
+rewrite !app_assoc.
f_equal.
f_equal.

@@ -758,7 +758,7 @@

Verif_strlibString functions< rewrite <- Zrepeat_app by lia.
replace (n-i) with (1 + (n-(i+1))) by lia.
rewrite <- Zrepeat_app by lia.
-rewrite !app_ass.
+rewrite <- !app_assoc.
Check split2_data_at_Tarray_app.
(*  forall (cs : compspecs) (mid n : Z) (sh : Share.t) 
    (t : type) (v1 v2 : list (reptype t)) (p : val),
@@ -895,11 +895,11 @@

Verif_strlibString functions<   PRE [ ]
    PROP ()
    PARAMS() GLOBALS (gv)
-    SEP (cstring Ews (Hello' ++ [Byte.zero]) (gv ___stringlit_1))
+    SEP (cstring Ews Hello' (gv ___stringlit_1))
  POST [ tint ]
    PROP ()
    RETURN (Vint (Int.repr (Z.of_N (Ascii.N_of_ascii "H"%char))))
-    SEP (cstring Ews (Hello' ++ [Byte.zero]) (gv ___stringlit_1)).
+    SEP (cstring Ews Hello' (gv ___stringlit_1)).
Lemma body_example_call_strcpy: semax_body Vprog Gprog
         f_example_call_strcpy example_call_strcpy_spec.
Proof.
@@ -936,7 +936,7 @@

Verif_strlibString functions<
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_strlib.v b/vc-current/Verif_strlib.v index ab4a79484..98275930e 100644 --- a/vc-current/Verif_strlib.v +++ b/vc-current/Verif_strlib.v @@ -430,7 +430,7 @@ Check Zrepeat_app. (* Hint: this lemma will be useful. *) Check upd_Znth_app1. (* Hint: this lemma will be useful. *) Check app_Znth2. (* Hint: this lemma will be useful. *) Check Znth_0_cons. (* Hint: this lemma will be useful. *) -(* Other useful lemmas will be map_app, app_ass *) +(* Other useful lemmas will be map_app, app_assoc *) (* FILL IN HERE *) Admitted. (** [] *) @@ -452,7 +452,7 @@ intros. apply derives_refl'. f_equal. (** Useful lemmas here will be: upd_Znth_app2, sublist_split, -repeat_app', app_Znth1, map_app, app_ass, sublist_len_1. *) +repeat_app', app_Znth1, map_app, app_assoc, sublist_len_1. *) (* FILL IN HERE *) Admitted. (** [] *) @@ -485,7 +485,7 @@ f_equal. rewrite <- Zrepeat_app by lia. replace (n-i) with (1 + (n-(i+1))) by lia. rewrite <- Zrepeat_app by lia. -rewrite !app_ass. +rewrite !app_assoc. f_equal. f_equal. (** Oops! The current proof goal is False! The problem was @@ -507,7 +507,7 @@ intros. rewrite <- Zrepeat_app by lia. replace (n-i) with (1 + (n-(i+1))) by lia. rewrite <- Zrepeat_app by lia. -rewrite !app_ass. +rewrite <- !app_assoc. Check split2_data_at_Tarray_app. (* forall (cs : compspecs) (mid n : Z) (sh : Share.t) (t : type) (v1 v2 : list (reptype t)) (p : val), @@ -603,11 +603,11 @@ Definition example_call_strcpy_spec := PRE [ ] PROP () PARAMS() GLOBALS (gv) - SEP (cstring Ews (Hello' ++ [Byte.zero]) (gv ___stringlit_1)) + SEP (cstring Ews Hello' (gv ___stringlit_1)) POST [ tint ] PROP () RETURN (Vint (Int.repr (Z.of_N (Ascii.N_of_ascii "H"%char)))) - SEP (cstring Ews (Hello' ++ [Byte.zero]) (gv ___stringlit_1)). + SEP (cstring Ews Hello' (gv ___stringlit_1)). Lemma body_example_call_strcpy: semax_body Vprog Gprog f_example_call_strcpy example_call_strcpy_spec. @@ -628,4 +628,4 @@ Lemma body_strcmp: semax_body Vprog Gprog f_strcmp strcmp_spec. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_sumarray.html b/vc-current/Verif_sumarray.html index a9ffa5cfe..e3341b959 100644 --- a/vc-current/Verif_sumarray.html +++ b/vc-current/Verif_sumarray.html @@ -1175,7 +1175,7 @@

Verif_sumarrayIntroduction to Verifi
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_sumarray.v b/vc-current/Verif_sumarray.v index 572d74ef1..26dbce3da 100644 --- a/vc-current/Verif_sumarray.v +++ b/vc-current/Verif_sumarray.v @@ -777,4 +777,4 @@ Qed. (** Recommended: read VC.pdf Chapters 23-49 (up to _Pointer comparisons_) *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/Verif_triang.html b/vc-current/Verif_triang.html index 2f1c53a50..2ac82ffaf 100644 --- a/vc-current/Verif_triang.html +++ b/vc-current/Verif_triang.html @@ -684,7 +684,7 @@

Verif_triangA client of the stack fu
-(* 2024-07-10 18:47 *)
+(* 2024-08-08 20:41 *)
diff --git a/vc-current/Verif_triang.v b/vc-current/Verif_triang.v index 36807503a..9f8acd044 100644 --- a/vc-current/Verif_triang.v +++ b/vc-current/Verif_triang.v @@ -482,4 +482,4 @@ sep_apply (create_mem_mgr gv). (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/append.v b/vc-current/append.v index c74b0b17d..1970e0bc7 100644 --- a/vc-current/append.v +++ b/vc-current/append.v @@ -486,4 +486,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/hash.v b/vc-current/hash.v index f92671f63..977b123e0 100644 --- a/vc-current/hash.v +++ b/vc-current/hash.v @@ -884,4 +884,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/hints.v b/vc-current/hints.v index 8a8602659..9b872c8fa 100644 --- a/vc-current/hints.v +++ b/vc-current/hints.v @@ -51,4 +51,4 @@ Ltac vc_special_hint := Ltac hint_special ::= try vc_special_hint. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/index.html b/vc-current/index.html index ae6c5157a..72ca50de6 100644 --- a/vc-current/index.html +++ b/vc-current/index.html @@ -44,7 +44,7 @@
Read

Download
-

Version 1.2.2 (2024-07-10 18:50, Coq 8.17.1)
+

Version 1.2.2 (2024-08-08 20:44, Coq 8.17.1)
Compatible with VST 2.11.1

diff --git a/vc-current/main2.v b/vc-current/main2.v index 2490a382f..056ebbf69 100644 --- a/vc-current/main2.v +++ b/vc-current/main2.v @@ -422,4 +422,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/reverse.v b/vc-current/reverse.v index 6838dbb45..30947754a 100644 --- a/vc-current/reverse.v +++ b/vc-current/reverse.v @@ -494,4 +494,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/stack.v b/vc-current/stack.v index 2cd50d1ce..fdae0db0b 100644 --- a/vc-current/stack.v +++ b/vc-current/stack.v @@ -608,4 +608,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/stack2.v b/vc-current/stack2.v index a2dcf665c..4ca156dcb 100644 --- a/vc-current/stack2.v +++ b/vc-current/stack2.v @@ -534,4 +534,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/stdlib.v b/vc-current/stdlib.v index 514322102..dd8cd74d9 100644 --- a/vc-current/stdlib.v +++ b/vc-current/stdlib.v @@ -390,4 +390,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/stdlib2.v b/vc-current/stdlib2.v index e8b460942..3fad0c843 100644 --- a/vc-current/stdlib2.v +++ b/vc-current/stdlib2.v @@ -500,4 +500,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/strlib.v b/vc-current/strlib.v index dee40f8b4..1cda1cf32 100644 --- a/vc-current/strlib.v +++ b/vc-current/strlib.v @@ -624,4 +624,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/sumarray.v b/vc-current/sumarray.v index 9bc57c0cd..f39ff8310 100644 --- a/vc-current/sumarray.v +++ b/vc-current/sumarray.v @@ -433,4 +433,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/triang2.v b/vc-current/triang2.v index 907fe53da..50d637135 100644 --- a/vc-current/triang2.v +++ b/vc-current/triang2.v @@ -507,4 +507,4 @@ Definition prog : Clight.program := mkprogram composites global_definitions public_idents _main Logic.I. -(* 2024-07-10 18:47 *) +(* 2024-08-08 20:41 *) diff --git a/vc-current/vc.tgz b/vc-current/vc.tgz index 38b71bc83..bd0440b58 100644 Binary files a/vc-current/vc.tgz and b/vc-current/vc.tgz differ diff --git a/vfa-current/ADT.html b/vfa-current/ADT.html index 4bcfbebf6..989cbe7d3 100644 --- a/vfa-current/ADT.html +++ b/vfa-current/ADT.html @@ -1732,7 +1732,7 @@

ADTAbstract Data Types

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/ADT.v b/vfa-current/ADT.v index 0fc78850c..00ce19324 100644 --- a/vfa-current/ADT.v +++ b/vfa-current/ADT.v @@ -1494,4 +1494,4 @@ End TreeETableSubset. Definition manual_grade_for_ListsETable : option (nat*string) := None. (** [] *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/ADTTest.v b/vfa-current/ADTTest.v index e07cbb307..5b45b5990 100644 --- a/vfa-current/ADTTest.v +++ b/vfa-current/ADTTest.v @@ -469,4 +469,4 @@ idtac "---------- ListsETable ---------". idtac "MANUAL". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/BagPerm.html b/vfa-current/BagPerm.html index 2671f7e84..f782a80b2 100644 --- a/vfa-current/BagPerm.html +++ b/vfa-current/BagPerm.html @@ -333,7 +333,7 @@

BagPermInsertion Sort With Bags -(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/BagPerm.v b/vfa-current/BagPerm.v index 3836fb013..619e0d4d2 100644 --- a/vfa-current/BagPerm.v +++ b/vfa-current/BagPerm.v @@ -189,4 +189,4 @@ Qed. (** $Date$ *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/BagPermTest.v b/vfa-current/BagPermTest.v index 01e9e39ed..c51b38721 100644 --- a/vfa-current/BagPermTest.v +++ b/vfa-current/BagPermTest.v @@ -243,4 +243,4 @@ idtac "---------- bag_perm ---------". Print Assumptions bag_perm. Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Binom.html b/vfa-current/Binom.html index 08597abe7..6ccce7397 100644 --- a/vfa-current/Binom.html +++ b/vfa-current/Binom.html @@ -609,7 +609,7 @@

BinomBinomial Queues

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Binom.v b/vfa-current/Binom.v index 14cb89cea..b146e0e25 100644 --- a/vfa-current/Binom.v +++ b/vfa-current/Binom.v @@ -397,4 +397,4 @@ End BinomQueue. *) (** [] *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/BinomTest.v b/vfa-current/BinomTest.v index a09dde8a6..17a308f61 100644 --- a/vfa-current/BinomTest.v +++ b/vfa-current/BinomTest.v @@ -252,4 +252,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Color.html b/vfa-current/Color.html index 5ad300bf9..81c16260a 100644 --- a/vfa-current/Color.html +++ b/vfa-current/Color.html @@ -854,7 +854,7 @@

ColorGraph Coloring

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Color.v b/vfa-current/Color.v index e7936d434..0142a7b48 100644 --- a/vfa-current/Color.v +++ b/vfa-current/Color.v @@ -599,4 +599,4 @@ Compute (M.elements (color palette G)). (* = [(4, 1); (2, 3); (6, 2); (1, 2); (5 nodes [6] and [1] with [2], and node [5] with color [1]. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/ColorTest.v b/vfa-current/ColorTest.v index 7ed8d2ca0..dcfd26611 100644 --- a/vfa-current/ColorTest.v +++ b/vfa-current/ColorTest.v @@ -323,4 +323,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Decide.html b/vfa-current/Decide.html index 79bc55b2a..f5b6d361e 100644 --- a/vfa-current/Decide.html +++ b/vfa-current/Decide.html @@ -734,7 +734,7 @@

DecideProgramming with Decision Proc
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Decide.v b/vfa-current/Decide.v index 2925b887e..e546d4654 100644 --- a/vfa-current/Decide.v +++ b/vfa-current/Decide.v @@ -503,4 +503,4 @@ simpl. it does. Either of these two methods is a reasonable way of programming with proof. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/DecideTest.v b/vfa-current/DecideTest.v index fa82f0fd1..dc23b8493 100644 --- a/vfa-current/DecideTest.v +++ b/vfa-current/DecideTest.v @@ -104,4 +104,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Extract.html b/vfa-current/Extract.html index 7b7e651cf..fcbb62571 100644 --- a/vfa-current/Extract.html +++ b/vfa-current/Extract.html @@ -535,7 +535,7 @@

ExtractRunning Coq Programs in OCaml
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Extract.v b/vfa-current/Extract.v index f4aeef9ee..2e9b39d41 100644 --- a/vfa-current/Extract.v +++ b/vfa-current/Extract.v @@ -388,4 +388,4 @@ Insert and lookup 20000 consecutive integers in 0.387535 seconds. balanced search trees to achieve logarithmic. [Redblack] will do that. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/ExtractTest.v b/vfa-current/ExtractTest.v index 6cacdc22f..bab759d64 100644 --- a/vfa-current/ExtractTest.v +++ b/vfa-current/ExtractTest.v @@ -120,4 +120,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Maps.html b/vfa-current/Maps.html index 0c8c29cff..52614b28a 100644 --- a/vfa-current/Maps.html +++ b/vfa-current/Maps.html @@ -349,7 +349,7 @@

MapsTotal and Partial Maps
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Maps.v b/vfa-current/Maps.v index b326c7388..5d52a7c39 100644 --- a/vfa-current/Maps.v +++ b/vfa-current/Maps.v @@ -217,4 +217,4 @@ Proof. apply t_update_permute. Qed. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/MapsTest.v b/vfa-current/MapsTest.v index d50db1486..f2ae32993 100644 --- a/vfa-current/MapsTest.v +++ b/vfa-current/MapsTest.v @@ -167,4 +167,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Merge.html b/vfa-current/Merge.html index af7821d2f..2c7b9016e 100644 --- a/vfa-current/Merge.html +++ b/vfa-current/Merge.html @@ -728,7 +728,7 @@

MergeMerge Sort, With Specification
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Merge.v b/vfa-current/Merge.v index c112441fb..370a62fdd 100644 --- a/vfa-current/Merge.v +++ b/vfa-current/Merge.v @@ -523,4 +523,4 @@ Qed. (** $Date$ *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/MergeTest.v b/vfa-current/MergeTest.v index b8603f447..6e03e38ef 100644 --- a/vfa-current/MergeTest.v +++ b/vfa-current/MergeTest.v @@ -171,4 +171,4 @@ idtac "---------- mergesort_perm ---------". Print Assumptions mergesort_perm. Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Multiset.html b/vfa-current/Multiset.html index ec09f23b7..48eef4590 100644 --- a/vfa-current/Multiset.html +++ b/vfa-current/Multiset.html @@ -542,7 +542,7 @@

MultisetInsertion Sort Verified With
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Multiset.v b/vfa-current/Multiset.v index 18a33a69d..1de935751 100644 --- a/vfa-current/Multiset.v +++ b/vfa-current/Multiset.v @@ -320,4 +320,4 @@ Proof. (** That means we can verify sorting algorithms using either permutations or multisets, whichever we find more convenient. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/MultisetTest.v b/vfa-current/MultisetTest.v index 82e06a1b4..66f8ef337 100644 --- a/vfa-current/MultisetTest.v +++ b/vfa-current/MultisetTest.v @@ -288,4 +288,4 @@ idtac "---------- contents_perm ---------". Print Assumptions contents_perm. Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Perm.html b/vfa-current/Perm.html index dffa38328..907f82c65 100644 --- a/vfa-current/Perm.html +++ b/vfa-current/Perm.html @@ -903,7 +903,7 @@

PermBasic Techniques for Comparisons
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Perm.v b/vfa-current/Perm.v index 6f3c3e45b..e939296e0 100644 --- a/vfa-current/Perm.v +++ b/vfa-current/Perm.v @@ -627,4 +627,4 @@ Proof. [maybe_swap_correct] will be applied (at a larger scale) in the next few chapters. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/PermTest.v b/vfa-current/PermTest.v index cfb1affe5..14d25ece4 100644 --- a/vfa-current/PermTest.v +++ b/vfa-current/PermTest.v @@ -128,4 +128,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Preface.html b/vfa-current/Preface.html index 3bc44945b..553cb02b9 100644 --- a/vfa-current/Preface.html +++ b/vfa-current/Preface.html @@ -281,7 +281,7 @@

Preface

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Preface.v b/vfa-current/Preface.v index 142afdc5d..8f2976138 100644 --- a/vfa-current/Preface.v +++ b/vfa-current/Preface.v @@ -162,4 +162,4 @@ NSF Expeditions grant 1521523, _The Science of Deep Specification_. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/PrefaceTest.v b/vfa-current/PrefaceTest.v index 4b85a1ee6..901b67d2a 100644 --- a/vfa-current/PrefaceTest.v +++ b/vfa-current/PrefaceTest.v @@ -72,4 +72,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Priqueue.html b/vfa-current/Priqueue.html index c334fb985..356158273 100644 --- a/vfa-current/Priqueue.html +++ b/vfa-current/Priqueue.html @@ -396,7 +396,7 @@

PriqueuePriority Queues

End List_Priqueue.
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Priqueue.v b/vfa-current/Priqueue.v index ce57a8ed8..f5d14a3d2 100644 --- a/vfa-current/Priqueue.v +++ b/vfa-current/Priqueue.v @@ -270,4 +270,4 @@ Proof. End List_Priqueue. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/PriqueueTest.v b/vfa-current/PriqueueTest.v index 59eab5036..a36d9eb6c 100644 --- a/vfa-current/PriqueueTest.v +++ b/vfa-current/PriqueueTest.v @@ -173,4 +173,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Redblack.html b/vfa-current/Redblack.html index 0772e2ff4..06fe125f8 100644 --- a/vfa-current/Redblack.html +++ b/vfa-current/Redblack.html @@ -1092,7 +1092,7 @@

RedblackRed-Black Trees

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Redblack.v b/vfa-current/Redblack.v index 020e64bc0..ad6715244 100644 --- a/vfa-current/Redblack.v +++ b/vfa-current/Redblack.v @@ -835,4 +835,4 @@ On the same machine that prints, - Red-black trees are about as fast on consecutive insertions as on random. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/RedblackTest.v b/vfa-current/RedblackTest.v index 6e7656903..7a3d96eba 100644 --- a/vfa-current/RedblackTest.v +++ b/vfa-current/RedblackTest.v @@ -304,4 +304,4 @@ idtac "---------- redblack_bound ---------". idtac "MANUAL". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/SearchTree.html b/vfa-current/SearchTree.html index 877d97fe8..14de4df71 100644 --- a/vfa-current/SearchTree.html +++ b/vfa-current/SearchTree.html @@ -1965,7 +1965,7 @@

SearchTreeBinary Search Trees
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/SearchTree.v b/vfa-current/SearchTree.v index f4daff453..024435c42 100644 --- a/vfa-current/SearchTree.v +++ b/vfa-current/SearchTree.v @@ -1323,4 +1323,4 @@ Proof. efficiently inside Coq. We'll explore [extraction] in [Extract]. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/SearchTreeTest.v b/vfa-current/SearchTreeTest.v index 00fe40ed8..7885059ed 100644 --- a/vfa-current/SearchTreeTest.v +++ b/vfa-current/SearchTreeTest.v @@ -293,4 +293,4 @@ idtac "---------- sorted_elements ---------". Print Assumptions sorted_elements. Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/Selection.html b/vfa-current/Selection.html index 9a052f24a..419820352 100644 --- a/vfa-current/Selection.html +++ b/vfa-current/Selection.html @@ -711,7 +711,7 @@

SelectionSelection Sort

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Selection.v b/vfa-current/Selection.v index 43c91a8b2..355327b3c 100644 --- a/vfa-current/Selection.v +++ b/vfa-current/Selection.v @@ -459,4 +459,4 @@ Proof. (* FILL IN HERE *) Admitted. (** [] *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/SelectionTest.v b/vfa-current/SelectionTest.v index 1efcc3909..28051a4bd 100644 --- a/vfa-current/SelectionTest.v +++ b/vfa-current/SelectionTest.v @@ -318,4 +318,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Sort.html b/vfa-current/Sort.html index 64e833e42..29c6f2084 100644 --- a/vfa-current/Sort.html +++ b/vfa-current/Sort.html @@ -512,7 +512,7 @@

SortInsertion Sort

-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Sort.v b/vfa-current/Sort.v index 0791f363c..40201b904 100644 --- a/vfa-current/Sort.v +++ b/vfa-current/Sort.v @@ -304,4 +304,4 @@ Qed. difficulty of the correctness proofs_. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/SortTest.v b/vfa-current/SortTest.v index aab450cf2..cb953efaa 100644 --- a/vfa-current/SortTest.v +++ b/vfa-current/SortTest.v @@ -175,4 +175,4 @@ idtac "---------- sorted'_sorted ---------". Print Assumptions sorted'_sorted. Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/Trie.html b/vfa-current/Trie.html index b0c269b7a..8ba65260e 100644 --- a/vfa-current/Trie.html +++ b/vfa-current/Trie.html @@ -918,7 +918,7 @@

TrieNumber Representations and Effic
-(* 2024-07-10 18:46 *)
+(* 2024-08-08 20:39 *)
diff --git a/vfa-current/Trie.v b/vfa-current/Trie.v index d0d1907ef..ab221e6e9 100644 --- a/vfa-current/Trie.v +++ b/vfa-current/Trie.v @@ -705,4 +705,4 @@ try (apply empty_relate). but [FMaps] uses different names for the functions [insert] and [lookup], and also provides several other operations on maps. *) -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:39 *) diff --git a/vfa-current/TrieTest.v b/vfa-current/TrieTest.v index a9e43d05d..68fb152a6 100644 --- a/vfa-current/TrieTest.v +++ b/vfa-current/TrieTest.v @@ -274,4 +274,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* 2024-07-10 18:46 *) +(* 2024-08-08 20:40 *) diff --git a/vfa-current/index.html b/vfa-current/index.html index 1541be1e5..d31d8554e 100644 --- a/vfa-current/index.html +++ b/vfa-current/index.html @@ -46,7 +46,7 @@
Download
-

Version 1.5.4 (2024-07-10 18:50, Coq 8.17.1 or later)

+

Version 1.5.4 (2024-08-08 20:44, Coq 8.17.1 or later)

diff --git a/vfa-current/vfa.tgz b/vfa-current/vfa.tgz index b8870fc1f..16ef647c9 100644 Binary files a/vfa-current/vfa.tgz and b/vfa-current/vfa.tgz differ