diff --git a/lf-current/Auto.html b/lf-current/Auto.html index 4a610637..03b35c48 100644 --- a/lf-current/Auto.html +++ b/lf-current/Auto.html @@ -17,7 +17,7 @@
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/Auto.v b/lf-current/Auto.v index 6673d10b..6847e903 100644 --- a/lf-current/Auto.v +++ b/lf-current/Auto.v @@ -601,4 +601,4 @@ Proof. eauto. Qed. [e] 开头的变体。 *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/AutoTest.v b/lf-current/AutoTest.v index 8a37742d..bbf39b05 100644 --- a/lf-current/AutoTest.v +++ b/lf-current/AutoTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:05 UTC 2019 *) +(* Sun Feb 17 18:24:32 UTC 2019 *) diff --git a/lf-current/Basics.html b/lf-current/Basics.html index 1d786475..5f3ca7e0 100644 --- a/lf-current/Basics.html +++ b/lf-current/Basics.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Basics.v b/lf-current/Basics.v index ab27e2bd..0d995f28 100644 --- a/lf-current/Basics.v +++ b/lf-current/Basics.v @@ -1198,4 +1198,4 @@ Fixpoint bin_to_nat (m:bin) : nat Definition manual_grade_for_binary : option (nat*string) := None. (** [] *) -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/BasicsTest.v b/lf-current/BasicsTest.v index e4bc6027..5241b0fd 100644 --- a/lf-current/BasicsTest.v +++ b/lf-current/BasicsTest.v @@ -192,4 +192,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:47 UTC 2019 *) +(* Sun Feb 17 18:24:14 UTC 2019 *) diff --git a/lf-current/Bib.html b/lf-current/Bib.html index e4c6af6a..52ad8a1a 100644 --- a/lf-current/Bib.html +++ b/lf-current/Bib.html @@ -17,7 +17,7 @@
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/Bib.v b/lf-current/Bib.v index a307c142..15919244 100644 --- a/lf-current/Bib.v +++ b/lf-current/Bib.v @@ -32,4 +32,4 @@ *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/BibTest.v b/lf-current/BibTest.v index 92479244..64537ee3 100644 --- a/lf-current/BibTest.v +++ b/lf-current/BibTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:05 UTC 2019 *) +(* Sun Feb 17 18:24:33 UTC 2019 *) diff --git a/lf-current/Extraction.html b/lf-current/Extraction.html index ee0b54ae..f3cadbb2 100644 --- a/lf-current/Extraction.html +++ b/lf-current/Extraction.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Extraction.v b/lf-current/Extraction.v index 520a73d8..8eab9244 100644 --- a/lf-current/Extraction.v +++ b/lf-current/Extraction.v @@ -116,4 +116,4 @@ Extraction "imp.ml" empty_st ceval_step parse. (** 有关提取的更多详情见_'软件基础'_第三卷_'已验证的函数式算法'_中的 Extract 一章。 *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/ExtractionTest.v b/lf-current/ExtractionTest.v index 09813245..2558b70a 100644 --- a/lf-current/ExtractionTest.v +++ b/lf-current/ExtractionTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:03 UTC 2019 *) +(* Sun Feb 17 18:24:31 UTC 2019 *) diff --git a/lf-current/Imp.html b/lf-current/Imp.html index b8ca84d8..cfef16f8 100644 --- a/lf-current/Imp.html +++ b/lf-current/Imp.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Imp.v b/lf-current/Imp.v index ae925d7e..1eb27121 100644 --- a/lf-current/Imp.v +++ b/lf-current/Imp.v @@ -1718,4 +1718,4 @@ End BreakImp. [] *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/ImpCEvalFun.html b/lf-current/ImpCEvalFun.html index 13b13c6f..9e86e452 100644 --- a/lf-current/ImpCEvalFun.html +++ b/lf-current/ImpCEvalFun.html @@ -17,7 +17,7 @@
diff --git a/lf-current/ImpCEvalFun.v b/lf-current/ImpCEvalFun.v index 424b0501..fe7ad7b7 100644 --- a/lf-current/ImpCEvalFun.v +++ b/lf-current/ImpCEvalFun.v @@ -369,4 +369,4 @@ Proof. rewrite E1 in E2. inversion E2. reflexivity. omega. omega. Qed. -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/ImpCEvalFunTest.v b/lf-current/ImpCEvalFunTest.v index 449d22d5..1df5cdf9 100644 --- a/lf-current/ImpCEvalFunTest.v +++ b/lf-current/ImpCEvalFunTest.v @@ -85,4 +85,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:02 UTC 2019 *) +(* Sun Feb 17 18:24:30 UTC 2019 *) diff --git a/lf-current/ImpParser.html b/lf-current/ImpParser.html index beb55ef9..293981b5 100644 --- a/lf-current/ImpParser.html +++ b/lf-current/ImpParser.html @@ -17,7 +17,7 @@
diff --git a/lf-current/ImpParser.v b/lf-current/ImpParser.v index 4d000d29..eca0acde 100644 --- a/lf-current/ImpParser.v +++ b/lf-current/ImpParser.v @@ -454,4 +454,4 @@ Example eg2 : parse " "x" ::= "z")%imp. Proof. cbv. reflexivity. Qed. -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/ImpParserTest.v b/lf-current/ImpParserTest.v index 78c77b70..924e8e82 100644 --- a/lf-current/ImpParserTest.v +++ b/lf-current/ImpParserTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:01 UTC 2019 *) +(* Sun Feb 17 18:24:29 UTC 2019 *) diff --git a/lf-current/ImpTest.v b/lf-current/ImpTest.v index 29fd96b8..b991c131 100644 --- a/lf-current/ImpTest.v +++ b/lf-current/ImpTest.v @@ -246,4 +246,4 @@ idtac "---------- BreakImp.while_stops_on_break ---------". Print Assumptions BreakImp.while_stops_on_break. Abort. -(* Sat Jan 26 15:15:00 UTC 2019 *) +(* Sun Feb 17 18:24:27 UTC 2019 *) diff --git a/lf-current/IndPrinciples.html b/lf-current/IndPrinciples.html index 8af31c0d..e3a053a3 100644 --- a/lf-current/IndPrinciples.html +++ b/lf-current/IndPrinciples.html @@ -17,7 +17,7 @@
diff --git a/lf-current/IndPrinciples.v b/lf-current/IndPrinciples.v index df6f49b5..5c26e0ee 100644 --- a/lf-current/IndPrinciples.v +++ b/lf-current/IndPrinciples.v @@ -592,4 +592,4 @@ Check le_ind. 因此，根据 [le_S]，[n <= S o']。 [] *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/IndPrinciplesTest.v b/lf-current/IndPrinciplesTest.v index ac8abd2d..d548eeb6 100644 --- a/lf-current/IndPrinciplesTest.v +++ b/lf-current/IndPrinciplesTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:57 UTC 2019 *) +(* Sun Feb 17 18:24:24 UTC 2019 *) diff --git a/lf-current/IndProp.html b/lf-current/IndProp.html index 40bf6110..4a4eefcd 100644 --- a/lf-current/IndProp.html +++ b/lf-current/IndProp.html @@ -17,7 +17,7 @@
diff --git a/lf-current/IndProp.v b/lf-current/IndProp.v index c27ad891..16b3c42a 100644 --- a/lf-current/IndProp.v +++ b/lf-current/IndProp.v @@ -1831,4 +1831,4 @@ Proof. (* 请在此处解答 *) Admitted. (** [] *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/IndPropTest.v b/lf-current/IndPropTest.v index ccc9cae1..9a54d277 100644 --- a/lf-current/IndPropTest.v +++ b/lf-current/IndPropTest.v @@ -292,4 +292,4 @@ idtac "---------- filter_challenge ---------". idtac "MANUAL". Abort. -(* Sat Jan 26 15:14:54 UTC 2019 *) +(* Sun Feb 17 18:24:22 UTC 2019 *) diff --git a/lf-current/Induction.html b/lf-current/Induction.html index 7ebea673..2018e803 100644 --- a/lf-current/Induction.html +++ b/lf-current/Induction.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Induction.v b/lf-current/Induction.v index 350a2c8a..bb2dedf4 100644 --- a/lf-current/Induction.v +++ b/lf-current/Induction.v @@ -588,4 +588,4 @@ Definition manual_grade_for_binary_inverse_c : option (nat*string) := None. (** [] *) -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/InductionTest.v b/lf-current/InductionTest.v index 649553c2..0ce0fbf7 100644 --- a/lf-current/InductionTest.v +++ b/lf-current/InductionTest.v @@ -177,4 +177,4 @@ idtac "---------- binary_inverse_c ---------". idtac "MANUAL". Abort. -(* Sat Jan 26 15:14:48 UTC 2019 *) +(* Sun Feb 17 18:24:15 UTC 2019 *) diff --git a/lf-current/Lists.html b/lf-current/Lists.html index abb65d23..62b6a64b 100644 --- a/lf-current/Lists.html +++ b/lf-current/Lists.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Lists.v b/lf-current/Lists.v index b1c2ce49..741f4e47 100644 --- a/lf-current/Lists.v +++ b/lf-current/Lists.v @@ -1018,4 +1018,4 @@ Inductive baz : Type := Definition manual_grade_for_baz_num_elts : option (nat*string) := None. (** [] *) -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/ListsTest.v b/lf-current/ListsTest.v index 0f8df109..1af629df 100644 --- a/lf-current/ListsTest.v +++ b/lf-current/ListsTest.v @@ -473,4 +473,4 @@ idtac "---------- rev_injective ---------". idtac "MANUAL". Abort. -(* Sat Jan 26 15:14:49 UTC 2019 *) +(* Sun Feb 17 18:24:16 UTC 2019 *) diff --git a/lf-current/Logic.html b/lf-current/Logic.html index 1fc1de93..2222da3d 100644 --- a/lf-current/Logic.html +++ b/lf-current/Logic.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Logic.v b/lf-current/Logic.v index 9667f778..7b6a1f8e 100644 --- a/lf-current/Logic.v +++ b/lf-current/Logic.v @@ -1389,4 +1389,4 @@ Definition implies_to_or := forall P Q:Prop, [] *) -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/LogicTest.v b/lf-current/LogicTest.v index 5856ab32..f6f55267 100644 --- a/lf-current/LogicTest.v +++ b/lf-current/LogicTest.v @@ -390,4 +390,4 @@ idtac "---------- not_exists_dist ---------". Print Assumptions not_exists_dist. Abort. -(* Sat Jan 26 15:14:52 UTC 2019 *) +(* Sun Feb 17 18:24:19 UTC 2019 *) diff --git a/lf-current/Maps.html b/lf-current/Maps.html index 80668822..7fd1e6ad 100644 --- a/lf-current/Maps.html +++ b/lf-current/Maps.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Maps.v b/lf-current/Maps.v index 076a578a..a07fefa8 100644 --- a/lf-current/Maps.v +++ b/lf-current/Maps.v @@ -341,4 +341,4 @@ Proof. apply t_update_permute. Qed. -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/MapsTest.v b/lf-current/MapsTest.v index 3e78b902..d9e35c3b 100644 --- a/lf-current/MapsTest.v +++ b/lf-current/MapsTest.v @@ -75,4 +75,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:55 UTC 2019 *) +(* Sun Feb 17 18:24:22 UTC 2019 *) diff --git a/lf-current/Poly.html b/lf-current/Poly.html index db8e6d40..9a85abbf 100644 --- a/lf-current/Poly.html +++ b/lf-current/Poly.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Poly.v b/lf-current/Poly.v index 28e7c702..bba7f044 100644 --- a/lf-current/Poly.v +++ b/lf-current/Poly.v @@ -1060,4 +1060,4 @@ End Church. End Exercises. -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/PolyTest.v b/lf-current/PolyTest.v index 33a8e8d6..db6f5ba3 100644 --- a/lf-current/PolyTest.v +++ b/lf-current/PolyTest.v @@ -421,4 +421,4 @@ idtac "---------- Exercises.Church.exp_3 ---------". Print Assumptions Exercises.Church.exp_3. Abort. -(* Sat Jan 26 15:14:50 UTC 2019 *) +(* Sun Feb 17 18:24:17 UTC 2019 *) diff --git a/lf-current/Postscript.html b/lf-current/Postscript.html index ca6644df..3ac666d6 100644 --- a/lf-current/Postscript.html +++ b/lf-current/Postscript.html @@ -17,7 +17,7 @@
-(* Sat Jan 26 15:14:46 UTC 2019 *)
+(* Sun Feb 17 18:24:13 UTC 2019 *)
diff --git a/lf-current/Postscript.v b/lf-current/Postscript.v index f250cfb4..a5d4139b 100644 --- a/lf-current/Postscript.v +++ b/lf-current/Postscript.v @@ -81,4 +81,4 @@ https://deepspec.org/event/dsss17/index.html *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/PostscriptTest.v b/lf-current/PostscriptTest.v index f949d1cf..0a2e34bc 100644 --- a/lf-current/PostscriptTest.v +++ b/lf-current/PostscriptTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:15:05 UTC 2019 *) +(* Sun Feb 17 18:24:32 UTC 2019 *) diff --git a/lf-current/Preface.html b/lf-current/Preface.html index c49be78f..19888677 100644 --- a/lf-current/Preface.html +++ b/lf-current/Preface.html @@ -17,7 +17,7 @@
-(* Sat Jan 26 15:14:44 UTC 2019 *)
+(* Sun Feb 17 18:24:11 UTC 2019 *)
diff --git a/lf-current/Preface.v b/lf-current/Preface.v index e00cdcb2..f8a975b1 100644 --- a/lf-current/Preface.v +++ b/lf-current/Preface.v @@ -307,4 +307,4 @@ （National Science Foundation）在 NSF 科研赞助 1521523 号 _'深度规范科学'_ 下提供支持。 *) -(* Sat Jan 26 15:14:44 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/PrefaceTest.v b/lf-current/PrefaceTest.v index f5216847..17356654 100644 --- a/lf-current/PrefaceTest.v +++ b/lf-current/PrefaceTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:47 UTC 2019 *) +(* Sun Feb 17 18:24:13 UTC 2019 *) diff --git a/lf-current/ProofObjects.html b/lf-current/ProofObjects.html index 8cbbc502..92089204 100644 --- a/lf-current/ProofObjects.html +++ b/lf-current/ProofObjects.html @@ -17,7 +17,7 @@
diff --git a/lf-current/ProofObjects.v b/lf-current/ProofObjects.v index 88b91854..e1876a2a 100644 --- a/lf-current/ProofObjects.v +++ b/lf-current/ProofObjects.v @@ -531,4 +531,4 @@ End MyEquality. 略会将这个事实加入到上下文中。 *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/ProofObjectsTest.v b/lf-current/ProofObjectsTest.v index 113a272f..3e9040c2 100644 --- a/lf-current/ProofObjectsTest.v +++ b/lf-current/ProofObjectsTest.v @@ -85,4 +85,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:56 UTC 2019 *) +(* Sun Feb 17 18:24:23 UTC 2019 *) diff --git a/lf-current/Rel.html b/lf-current/Rel.html index f8ff3562..4fb1467f 100644 --- a/lf-current/Rel.html +++ b/lf-current/Rel.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Rel.v b/lf-current/Rel.v index be491428..40d69af5 100644 --- a/lf-current/Rel.v +++ b/lf-current/Rel.v @@ -356,4 +356,4 @@ Proof. (* 请在此处解答 *) Admitted. (** [] *) -(* Sat Jan 26 15:14:46 UTC 2019 *) +(* Sun Feb 17 18:24:12 UTC 2019 *) diff --git a/lf-current/RelTest.v b/lf-current/RelTest.v index eceadf04..1d57432c 100644 --- a/lf-current/RelTest.v +++ b/lf-current/RelTest.v @@ -44,4 +44,4 @@ idtac "". idtac "********** Advanced **********". Abort. -(* Sat Jan 26 15:14:58 UTC 2019 *) +(* Sun Feb 17 18:24:25 UTC 2019 *) diff --git a/lf-current/Tactics.html b/lf-current/Tactics.html index d034af32..b0f2b77d 100644 --- a/lf-current/Tactics.html +++ b/lf-current/Tactics.html @@ -17,7 +17,7 @@
diff --git a/lf-current/Tactics.v b/lf-current/Tactics.v index 809c4f4e..fe570cb6 100644 --- a/lf-current/Tactics.v +++ b/lf-current/Tactics.v @@ -1050,4 +1050,4 @@ Proof. (* 请在此处解答 *) Admitted. -(* Sat Jan 26 15:14:45 UTC 2019 *) +(* Sun Feb 17 18:24:11 UTC 2019 *) diff --git a/lf-current/TacticsTest.v b/lf-current/TacticsTest.v index cb7b2e5a..78860bde 100644 --- a/lf-current/TacticsTest.v +++ b/lf-current/TacticsTest.v @@ -219,4 +219,4 @@ idtac "---------- existsb_existsb' ---------". Print Assumptions existsb_existsb'. Abort. -(* Sat Jan 26 15:14:51 UTC 2019 *) +(* Sun Feb 17 18:24:18 UTC 2019 *) diff --git a/lf-current/coqindex.html b/lf-current/coqindex.html index 3262ae1a..43466505 100644 --- a/lf-current/coqindex.html +++ b/lf-current/coqindex.html @@ -17,7 +17,7 @@