r432

Coq-zh · Jun 8, 2020 · e1f470b · e1f470b
1 parent 1a4139b
commit e1f470b
Show file tree

Hide file tree

Showing 200 changed files with 202 additions and 202 deletions.
diff --git a/lf-current/AltAuto.html b/lf-current/AltAuto.html
@@ -1118,7 +1118,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">More Automation</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/AltAuto.v b/lf-current/AltAuto.v
@@ -842,4 +842,4 @@ Qed.
     the ordinary variants don't do the job. *)
 
 
-(* 2020-06-02 03:36:30 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/AltAutoTest.v b/lf-current/AltAutoTest.v
@@ -78,4 +78,4 @@ idtac "---------- pumping_redux ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2020-06-02 03:37:08 (UTC+00) *)
+(* 2020-06-08 10:48:16 (UTC+00) *)
diff --git a/lf-current/Auto.html b/lf-current/Auto.html
@@ -809,7 +809,7 @@ <h1 class="libtitle">Auto<span class="subtitle">更多的自动化</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Auto.v b/lf-current/Auto.v
@@ -609,4 +609,4 @@ Proof. info_eauto. Qed.
     [e] 开头的变体。 *)
 
 
-(* 2020-06-02 03:36:30 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/AutoTest.v b/lf-current/AutoTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:37:03 (UTC+00) *)
+(* 2020-06-08 10:48:12 (UTC+00) *)
diff --git a/lf-current/Basics.html b/lf-current/Basics.html
@@ -1797,7 +1797,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Coq 函数式编程</span></h1
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:26&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:33&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Basics.v b/lf-current/Basics.v
@@ -1264,4 +1264,4 @@ Example test_bin_incr6 :
 
 (** [] *)
 
-(* 2020-06-02 03:36:26 (UTC+00) *)
+(* 2020-06-08 10:47:33 (UTC+00) *)
diff --git a/lf-current/BasicsTest.v b/lf-current/BasicsTest.v
@@ -264,4 +264,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:33 (UTC+00) *)
+(* 2020-06-08 10:47:40 (UTC+00) *)
diff --git a/lf-current/Bib.html b/lf-current/Bib.html
@@ -87,7 +87,7 @@ <h1 class="libtitle">Bib<span class="subtitle">参考文献</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:31&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Bib.v b/lf-current/Bib.v
@@ -32,4 +32,4 @@
 
 *)
 
-(* 2020-06-02 03:36:31 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/BibTest.v b/lf-current/BibTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:37:08 (UTC+00) *)
+(* 2020-06-08 10:48:17 (UTC+00) *)
diff --git a/lf-current/Extraction.html b/lf-current/Extraction.html
@@ -236,7 +236,7 @@ <h1 class="libtitle">Extraction<span class="subtitle">从 Coq 中提取 ML</span
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Extraction.v b/lf-current/Extraction.v
@@ -116,4 +116,4 @@ Extraction "imp.ml" empty_st ceval_step parse.
 (** 有关提取的更多详情见_'软件基础'_第三卷_'已验证的函数式算法'_中的
     Extract 一章。 *)
 
-(* 2020-06-02 03:36:30 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/ExtractionTest.v b/lf-current/ExtractionTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:37:01 (UTC+00) *)
+(* 2020-06-08 10:48:10 (UTC+00) *)
diff --git a/lf-current/Imp.html b/lf-current/Imp.html
@@ -2576,7 +2576,7 @@ <h1 class="libtitle">Imp<span class="subtitle">简单的指令式程序</span></
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:29&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:37&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Imp.v b/lf-current/Imp.v
@@ -1723,4 +1723,4 @@ End BreakImp.
     [] *)
 
 
-(* 2020-06-02 03:36:29 (UTC+00) *)
+(* 2020-06-08 10:47:37 (UTC+00) *)
diff --git a/lf-current/ImpCEvalFun.html b/lf-current/ImpCEvalFun.html
@@ -472,7 +472,7 @@ <h1 class="libtitle">ImpCEvalFun<span class="subtitle">Imp 的求值函数</span
 </div>
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git 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.
 
-(* 2020-06-02 03:36:30 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/ImpCEvalFunTest.v b/lf-current/ImpCEvalFunTest.v
@@ -98,4 +98,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:59 (UTC+00) *)
+(* 2020-06-08 10:48:08 (UTC+00) *)
diff --git a/lf-current/ImpParser.html b/lf-current/ImpParser.html
@@ -544,7 +544,7 @@ <h1 class="libtitle">ImpParser<span class="subtitle">用 Coq 实现词法分析
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Imp.html#83a07334581e0deb166d05032f77769f"><span class="id" title="notation">END</span></a><a class="idref" href="Imp.html#5604146224f04ce8ff933bc02eb29824"><span class="id" title="notation">;;</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;"x" <a class="idref" href="Imp.html#1415d381b898f10db78e714a0a964c<sub>11</sub>"><span class="id" title="notation"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>:</span>:</span>=</span></span></a> "z")%<span class="id" title="var">imp</span>.<br/>
 <span class="id" title="keyword">Proof</span>. <span class="id" title="tactic">cbv</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/ImpParser.v b/lf-current/ImpParser.v
@@ -454,4 +454,4 @@ Example eg2 : parse "
       "x" ::= "z")%imp.
 Proof. cbv. reflexivity. Qed.
 
-(* 2020-06-02 03:36:30 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/ImpParserTest.v b/lf-current/ImpParserTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:57 (UTC+00) *)
+(* 2020-06-08 10:48:06 (UTC+00) *)
diff --git a/lf-current/ImpTest.v b/lf-current/ImpTest.v
@@ -249,4 +249,4 @@ idtac "---------- BreakImp.while_stops_on_break ---------".
 Print Assumptions BreakImp.while_stops_on_break.
 Abort.
 
-(* 2020-06-02 03:36:55 (UTC+00) *)
+(* 2020-06-08 10:48:04 (UTC+00) *)
diff --git a/lf-current/IndPrinciples.html b/lf-current/IndPrinciples.html
@@ -1253,7 +1253,7 @@ <h1 class="libtitle">IndPrinciples<span class="subtitle">归纳法则</span></h1
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:29&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:37&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/IndPrinciples.v b/lf-current/IndPrinciples.v
@@ -800,4 +800,4 @@ Qed.
     scratch.  Only lemmas whose proofs pass the type-checker can be
     used in further proof developments.  *)
 
-(* 2020-06-02 03:36:29 (UTC+00) *)
+(* 2020-06-08 10:47:37 (UTC+00) *)
diff --git a/lf-current/IndPrinciplesTest.v b/lf-current/IndPrinciplesTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:50 (UTC+00) *)
+(* 2020-06-08 10:47:58 (UTC+00) *)
diff --git a/lf-current/IndProp.html b/lf-current/IndProp.html
@@ -2996,7 +2996,7 @@ <h1 class="libtitle">IndProp<span class="subtitle">归纳定义的命题</span><
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:28&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:35&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/IndProp.v b/lf-current/IndProp.v
@@ -1971,4 +1971,4 @@ Proof.
   (* 请在此处解答 *) Admitted.
 (** [] *)
 
-(* 2020-06-02 03:36:28 (UTC+00) *)
+(* 2020-06-08 10:47:35 (UTC+00) *)
diff --git a/lf-current/IndPropTest.v b/lf-current/IndPropTest.v
@@ -305,4 +305,4 @@ idtac "---------- filter_challenge ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2020-06-02 03:36:45 (UTC+00) *)
+(* 2020-06-08 10:47:54 (UTC+00) *)
diff --git a/lf-current/Induction.html b/lf-current/Induction.html
@@ -886,7 +886,7 @@ <h1 class="libtitle">Induction<span class="subtitle">归纳证明</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:26&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:34&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Induction.v b/lf-current/Induction.v
@@ -587,4 +587,4 @@ Definition manual_grade_for_binary_inverse_b : option (nat*string) := None.
 Definition manual_grade_for_binary_inverse_c : option (nat*string) := None.
 (** [] *)
 
-(* 2020-06-02 03:36:26 (UTC+00) *)
+(* 2020-06-08 10:47:34 (UTC+00) *)
diff --git a/lf-current/InductionTest.v b/lf-current/InductionTest.v
@@ -180,4 +180,4 @@ idtac "---------- binary_inverse_c ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2020-06-02 03:36:34 (UTC+00) *)
+(* 2020-06-08 10:47:42 (UTC+00) *)
diff --git a/lf-current/Lists.html b/lf-current/Lists.html
@@ -1468,7 +1468,7 @@ <h1 class="libtitle">Lists<span class="subtitle">使用结构化的数据</span>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:26&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:34&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Lists.v b/lf-current/Lists.v
@@ -1011,4 +1011,4 @@ Inductive baz : Type :=
 Definition manual_grade_for_baz_num_elts : option (nat*string) := None.
 (** [] *)
 
-(* 2020-06-02 03:36:26 (UTC+00) *)
+(* 2020-06-08 10:47:34 (UTC+00) *)
diff --git a/lf-current/ListsTest.v b/lf-current/ListsTest.v
@@ -486,4 +486,4 @@ idtac "---------- rev_injective ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2020-06-02 03:36:36 (UTC+00) *)
+(* 2020-06-08 10:47:44 (UTC+00) *)
diff --git a/lf-current/Logic.html b/lf-current/Logic.html
@@ -2070,7 +2070,7 @@ <h1 class="libtitle">Logic<span class="subtitle">Coq 中的逻辑系统</span></
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:27&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:35&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Logic.v b/lf-current/Logic.v
@@ -1411,4 +1411,4 @@ Definition implies_to_or := forall P Q:Prop,
 
     [] *)
 
-(* 2020-06-02 03:36:27 (UTC+00) *)
+(* 2020-06-08 10:47:35 (UTC+00) *)
diff --git a/lf-current/LogicTest.v b/lf-current/LogicTest.v
@@ -403,4 +403,4 @@ idtac "---------- not_exists_dist ---------".
 Print Assumptions not_exists_dist.
 Abort.
 
-(* 2020-06-02 03:36:42 (UTC+00) *)
+(* 2020-06-08 10:47:50 (UTC+00) *)
diff --git a/lf-current/Maps.html b/lf-current/Maps.html
@@ -552,7 +552,7 @@ <h1 class="libtitle">Maps<span class="subtitle">全映射与偏映射</span></h1
 </div>
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:29&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:36&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Maps.v b/lf-current/Maps.v
@@ -346,4 +346,4 @@ Proof.
   apply t_update_permute.
 Qed.
 
-(* 2020-06-02 03:36:29 (UTC+00) *)
+(* 2020-06-08 10:47:36 (UTC+00) *)
diff --git a/lf-current/MapsTest.v b/lf-current/MapsTest.v
@@ -88,4 +88,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:47 (UTC+00) *)
+(* 2020-06-08 10:47:55 (UTC+00) *)
diff --git a/lf-current/Poly.html b/lf-current/Poly.html
@@ -1627,7 +1627,7 @@ <h1 class="libtitle">Poly<span class="subtitle">多态与高阶函数</span></h1
 <br/>
 <span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises.Church"><span class="id" title="module">Church</span></a>.<br/><hr class='doublespaceincode'/>
 <span class="id" title="keyword">End</span> <a class="idref" href="Poly.html#Exercises"><span class="id" title="module">Exercises</span></a>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:27&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:34&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Poly.v b/lf-current/Poly.v
@@ -1039,4 +1039,4 @@ End Church.
 End Exercises.
 
 
-(* 2020-06-02 03:36:27 (UTC+00) *)
+(* 2020-06-08 10:47:34 (UTC+00) *)
diff --git a/lf-current/PolyTest.v b/lf-current/PolyTest.v
@@ -434,4 +434,4 @@ idtac "---------- Exercises.Church.exp_3 ---------".
 Print Assumptions Exercises.Church.exp_3.
 Abort.
 
-(* 2020-06-02 03:36:38 (UTC+00) *)
+(* 2020-06-08 10:47:46 (UTC+00) *)
diff --git a/lf-current/Postscript.html b/lf-current/Postscript.html
@@ -227,7 +227,7 @@ <h1 class="libtitle">Postscript<span class="subtitle">后记</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:31&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Postscript.v b/lf-current/Postscript.v
@@ -81,4 +81,4 @@
          https://deepspec.org/event/dsss17/index.html
 *)
 
-(* 2020-06-02 03:36:31 (UTC+00) *)
+(* 2020-06-08 10:47:38 (UTC+00) *)
diff --git a/lf-current/PostscriptTest.v b/lf-current/PostscriptTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:37:08 (UTC+00) *)
+(* 2020-06-08 10:48:17 (UTC+00) *)
diff --git a/lf-current/Preface.html b/lf-current/Preface.html
@@ -541,7 +541,7 @@ <h1 class="libtitle">Preface<span class="subtitle">前言</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:25&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:33&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Preface.v b/lf-current/Preface.v
@@ -327,4 +327,4 @@
     （National Science Foundation）在 NSF 科研赞助 1521523 号
     _'深度规范科学'_ 下提供支持。 *)
 
-(* 2020-06-02 03:36:25 (UTC+00) *)
+(* 2020-06-08 10:47:33 (UTC+00) *)
diff --git a/lf-current/PrefaceTest.v b/lf-current/PrefaceTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:31 (UTC+00) *)
+(* 2020-06-08 10:47:39 (UTC+00) *)
diff --git a/lf-current/ProofObjects.html b/lf-current/ProofObjects.html
@@ -852,7 +852,7 @@ <h1 class="libtitle">ProofObjects<span class="subtitle">柯里-霍华德对应</
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:29&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:36&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/ProofObjects.v b/lf-current/ProofObjects.v
@@ -530,4 +530,4 @@ End MyEquality.
     略会将这个事实加入到上下文中。 *)
 
 
-(* 2020-06-02 03:36:29 (UTC+00) *)
+(* 2020-06-08 10:47:36 (UTC+00) *)
diff --git a/lf-current/ProofObjectsTest.v b/lf-current/ProofObjectsTest.v
@@ -98,4 +98,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:48 (UTC+00) *)
+(* 2020-06-08 10:47:57 (UTC+00) *)
diff --git a/lf-current/Rel.html b/lf-current/Rel.html
@@ -612,7 +612,7 @@ <h1 class="libtitle">Rel<span class="subtitle">关系的性质</span></h1>
 <div class="code">
 
 <br/>
-<span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:29&nbsp;(UTC+00)&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:37&nbsp;(UTC+00)&nbsp;*)</span><br/>
 </div>
 </div>
 

diff --git a/lf-current/Rel.v b/lf-current/Rel.v
@@ -356,4 +356,4 @@ Proof.
   (* 请在此处解答 *) Admitted.
 (** [] *)
 
-(* 2020-06-02 03:36:29 (UTC+00) *)
+(* 2020-06-08 10:47:37 (UTC+00) *)
diff --git a/lf-current/RelTest.v b/lf-current/RelTest.v
@@ -57,4 +57,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2020-06-02 03:36:52 (UTC+00) *)
+(* 2020-06-08 10:48:00 (UTC+00) *)
-Original file line number
+Diff line change
@@ Expand Up @@
     <div class="code">
     <br/>
-    <span class="comment">(*&nbsp;2020-06-02&nbsp;03:36:30&nbsp;(UTC+00)&nbsp;*)</span><br/>
+    <span class="comment">(*&nbsp;2020-06-08&nbsp;10:47:38&nbsp;(UTC+00)&nbsp;*)</span><br/>
     </div>
     </div>
@@ Expand Down @@
Original file line number	Diff line number	Diff line change
Expand Up		@@ -842,4 +842,4 @@ Qed.
		the ordinary variants don't do the job. *)


		(* 2020-06-02 03:36:30 (UTC+00) *)
		(* 2020-06-08 10:47:38 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -609,4 +609,4 @@ Proof. info_eauto. Qed.
		[e] 开头的变体。 *)


		(* 2020-06-02 03:36:30 (UTC+00) *)
		(* 2020-06-08 10:47:38 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1264,4 +1264,4 @@ Example test_bin_incr6 :

		(** [] *)

		(* 2020-06-02 03:36:26 (UTC+00) *)
		(* 2020-06-08 10:47:33 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -32,4 +32,4 @@

		*)

		(* 2020-06-02 03:36:31 (UTC+00) *)
		(* 2020-06-08 10:47:38 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1723,4 +1723,4 @@ End BreakImp.
		[] *)


		(* 2020-06-02 03:36:29 (UTC+00) *)
		(* 2020-06-08 10:47:37 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1411,4 +1411,4 @@ Definition implies_to_or := forall P Q:Prop,

		[] *)

		(* 2020-06-02 03:36:27 (UTC+00) *)
		(* 2020-06-08 10:47:35 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -1039,4 +1039,4 @@ End Church.
		End Exercises.


		(* 2020-06-02 03:36:27 (UTC+00) *)
		(* 2020-06-08 10:47:34 (UTC+00) *)
Original file line number	Diff line number	Diff line change
Expand Up		@@ -530,4 +530,4 @@ End MyEquality.
		略会将这个事实加入到上下文中。 *)


		(* 2020-06-02 03:36:29 (UTC+00) *)
		(* 2020-06-08 10:47:36 (UTC+00) *)