r207

Coq-zh · Dec 7, 2018 · 8ce2ec8 · 8ce2ec8
1 parent 600610a
commit 8ce2ec8
Show file tree

Hide file tree

Showing 14 changed files with 899 additions and 1,213 deletions.
diff --git a/lf-current/index.html b/lf-current/index.html
@@ -84,7 +84,7 @@
             <div class="button"><a href="toc.html">阅读</a></div><br />
             <div class="button"><a href="lf.tgz">下载</a></div>
           </div>
-          <p>版本 5.6 (19 Nov 2018, Coq 8.8.0)</p>
+          <p>版本 5.6 (07 Dec 2018, Coq 8.8.0)</p>
 
         </div>
       </div>

diff --git a/lf-current/lf.tgz b/lf-current/lf.tgz
diff --git a/plf-current/MoreStlc.html b/plf-current/MoreStlc.html
diff --git a/plf-current/MoreStlc.v b/plf-current/MoreStlc.v
diff --git a/plf-current/Smallstep.html b/plf-current/Smallstep.html
@@ -335,7 +335,7 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 </div>
 
 <div class="doc">
-本章中，我们主要的例子将会是单步规约关系，<span class="inlinecode">==&gt;</span>，以及它的多步版本，
+本章中，我们主要的例子将会是单步归约关系，<span class="inlinecode">==&gt;</span>，以及它的多步版本，
     <span class="inlinecode">==&gt;*</span>（后面会定义），但是也有许多其他例子——比如，“等于”、“小于”、“小于等于”
     和数字上“平方数”关系，还有字符串和列表的“前缀”关系。
 <div class="paragraph"> </div>
@@ -491,7 +491,7 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 
 <div class="paragraph"> </div>
 
- 下一步，我们会使用“值”的概念来稍微重新表述一下单步规约的定义。
+ 下一步，我们会使用“值”的概念来稍微重新表述一下单步归约的定义。
 <div class="paragraph"> </div>
 
  为了更好地理解 <span class="inlinecode">==&gt;</span> 关系，我们定义一个<b>抽象机（abstract machine）</b>:
@@ -535,7 +535,7 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 
 
 </li>
-<li> 当无法继续进行规约时，<b>输出（read out）</b>最终的机器状态作为执行的结果。  
+<li> 当无法继续进行归约时，<b>输出（read out）</b>最终的机器状态作为执行的结果。  
 </li>
 </ul>
 
@@ -683,8 +683,8 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 
 <div class="paragraph"> </div>
 
- 这个玩具语言的单步规约定义是十分简单的，但是对于大一点的语言，往往会出现
-    因为忘记某个规则而导致一些项虽然还不是值但已无法继续前进规约的情况。下面的定理
+ 这个玩具语言的单步归约定义是十分简单的，但是对于大一点的语言，往往会出现
+    因为忘记某个规则而导致一些项虽然还不是值但已无法继续前进归约的情况。下面的定理
     说明了我们没有犯这样的错误。 
 <div class="paragraph"> </div>
 
@@ -779,7 +779,7 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 
 <div class="doc">
 请注意这个定义规范了对任意集合 <span class="inlinecode"><span class="id" type="var">X</span></span> 上的任意关系 <span class="inlinecode"><span class="id" type="var">R</span></span> 的正规式，而不仅仅是我们
-    这里关心的某个单步规约关系的正规式。后面的课程讨论其他关系时我们会继续使用这个术语。 
+    这里关心的某个单步归约关系的正规式。后面的课程讨论其他关系时我们会继续使用这个术语。 
 <div class="paragraph"> </div>
 
  我们可以使用这个术语来一般化对于强可进性定理的观察：在这个语言中，
@@ -1162,7 +1162,7 @@ <h1 class="libtitle">Smallstep<span class="subtitle">小步操作语义</span></
 </div>
 
 <div class="doc">
-<a name="lab148"></a><h1 class="section">多步规约</h1>
+<a name="lab148"></a><h1 class="section">多步归约</h1>
 
 <div class="paragraph"> </div>
 

diff --git a/plf-current/Smallstep.v b/plf-current/Smallstep.v
@@ -179,7 +179,7 @@ End SimpleArith1.
 
 Definition relation (X: Type) := X -> X -> Prop.
 
-(** 本章中，我们主要的例子将会是单步规约关系，[==>]，以及它的多步版本，
+(** 本章中，我们主要的例子将会是单步归约关系，[==>]，以及它的多步版本，
     [==>*]（后面会定义），但是也有许多其他例子——比如，“等于”、“小于”、“小于等于”
     和数字上“平方数”关系，还有字符串和列表的“前缀”关系。*)
 
@@ -293,7 +293,7 @@ End SimpleArith3.
 (* ================================================================= *)
 (** ** 值 *)
 
-(** 下一步，我们会使用“值”的概念来稍微重新表述一下单步规约的定义。*)
+(** 下一步，我们会使用“值”的概念来稍微重新表述一下单步归约的定义。*)
 
 (** 为了更好地理解 [==>] 关系，我们定义一个_'抽象机（abstract machine）'_:
 
@@ -309,8 +309,8 @@ End SimpleArith3.
 
       - 重复使用 [==>] 关系来找到一个以 [t] 开始的机器状态序列，序列中每个状态
         会转移到下一个。
-
-      - 当无法继续进行规约时，_'输出（read out）'_最终的机器状态作为执行的结果。  *)
+      
+      - 当无法继续进行归约时，_'输出（read out）'_最终的机器状态作为执行的结果。  *)
 
 (** 直观地来说，可以看到机器的最终状态总是形如 [C n] 的项。
     我们把这些项叫做_'值（values）'_。 *)
@@ -388,8 +388,8 @@ Proof.
 (* ================================================================= *)
 (** ** 强可进性和正规式 *)
 
-(** 这个玩具语言的单步规约定义是十分简单的，但是对于大一点的语言，往往会出现
-    因为忘记某个规则而导致一些项虽然还不是值但已无法继续前进规约的情况。下面的定理
+(** 这个玩具语言的单步归约定义是十分简单的，但是对于大一点的语言，往往会出现
+    因为忘记某个规则而导致一些项虽然还不是值但已无法继续前进归约的情况。下面的定理
     说明了我们没有犯这样的错误。 *)
 
 (** _'定理'_（_'强可进性'_（Strong Progress））：如果 [t] 是一个项，那么 [t]
@@ -442,7 +442,7 @@ Definition normal_form {X:Type} (R:relation X) (t:X) : Prop :=
   ~ exists t', R t t'.
 
 (** 请注意这个定义规范了对任意集合 [X] 上的任意关系 [R] 的正规式，而不仅仅是我们
-    这里关心的某个单步规约关系的正规式。后面的课程讨论其他关系时我们会继续使用这个术语。 *)
+    这里关心的某个单步归约关系的正规式。后面的课程讨论其他关系时我们会继续使用这个术语。 *)
 
 (** 我们可以使用这个术语来一般化对于强可进性定理的观察：在这个语言中，
     正规式和值实际上是同一个东西。 *)
@@ -731,7 +731,7 @@ End Temp5.
 End Temp4.
 
 (* ################################################################# *)
-(** * 多步规约 *)
+(** * 多步归约 *)
 
 (** 目前为止，我们学习的是_'单步归约（single-step reduction）'_关系 [==>]，
     它形式化了抽象机执行程序的每一步。

diff --git a/plf-current/coqindex.html b/plf-current/coqindex.html
@@ -1388,14 +1388,14 @@ <h1>Global Index</h1>
 <a href="PLF.Smallstep.html#stack_step">stack_step</a> [inductive, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Smallstep.html#stack_step_deterministic">stack_step_deterministic</a> [lemma, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.RecordSub.html#step">step</a> [inductive, in <a href="PLF.RecordSub.html">PLF.RecordSub</a>]<br/>
-<a href="PLF.Smallstep.html#step">step</a> [inductive, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Norm.html#step">step</a> [inductive, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Types.html#step">step</a> [inductive, in <a href="PLF.Types.html">PLF.Types</a>]<br/>
 <a href="PLF.Sub.html#step">step</a> [inductive, in <a href="PLF.Sub.html">PLF.Sub</a>]<br/>
+<a href="PLF.Smallstep.html#step">step</a> [inductive, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Typechecking.html#StepFunction">StepFunction</a> [module, in <a href="PLF.Typechecking.html">PLF.Typechecking</a>]<br/>
 <a href="PLF.Types.html#step_deterministic">step_deterministic</a> [lemma, in <a href="PLF.Types.html">PLF.Types</a>]<br/>
-<a href="PLF.Norm.html#step_deterministic">step_deterministic</a> [lemma, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#step_deterministic">step_deterministic</a> [lemma, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
+<a href="PLF.Norm.html#step_deterministic">step_deterministic</a> [lemma, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#step_normalizing">step_normalizing</a> [lemma, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Smallstep.html#step_normal_form">step_normal_form</a> [definition, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Norm.html#step_normal_form">step_normal_form</a> [abbreviation, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
@@ -1631,8 +1631,8 @@ <h1>Global Index</h1>
 <a href="PLF.MoreStlc.html#STLCExtended.tsnd">STLCExtended.tsnd</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.tsucc">STLCExtended.tsucc</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.TSum">STLCExtended.TSum</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
-<a href="PLF.MoreStlc.html#STLCExtended.tunit">STLCExtended.tunit</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.TUnit">STLCExtended.TUnit</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
+<a href="PLF.MoreStlc.html#STLCExtended.tunit">STLCExtended.tunit</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.tvar">STLCExtended.tvar</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.ty">STLCExtended.ty</a> [inductive, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.T_Abs">STLCExtended.T_Abs</a> [constructor, in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
@@ -2185,8 +2185,8 @@ <h1>Global Index</h1>
 <a href="PLF.RecordSub.html#value">value</a> [inductive, in <a href="PLF.RecordSub.html">PLF.RecordSub</a>]<br/>
 <a href="PLF.Sub.html#value">value</a> [inductive, in <a href="PLF.Sub.html">PLF.Sub</a>]<br/>
 <a href="PLF.Types.html#value">value</a> [definition, in <a href="PLF.Types.html">PLF.Types</a>]<br/>
-<a href="PLF.Norm.html#value">value</a> [inductive, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#value">value</a> [inductive, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
+<a href="PLF.Norm.html#value">value</a> [inductive, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Norm.html#value_halts">value_halts</a> [lemma, in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Types.html#value_is_nf">value_is_nf</a> [lemma, in <a href="PLF.Types.html">PLF.Types</a>]<br/>
 <a href="PLF.Smallstep.html#value_is_nf">value_is_nf</a> [lemma, in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
@@ -2933,8 +2933,8 @@ <h1>Constructor Index</h1>
 <a href="PLF.MoreStlc.html#STLCExtended.tsnd">STLCExtended.tsnd</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.tsucc">STLCExtended.tsucc</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.TSum">STLCExtended.TSum</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
-<a href="PLF.MoreStlc.html#STLCExtended.tunit">STLCExtended.tunit</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.TUnit">STLCExtended.TUnit</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
+<a href="PLF.MoreStlc.html#STLCExtended.tunit">STLCExtended.tunit</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.tvar">STLCExtended.tvar</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.T_Abs">STLCExtended.T_Abs</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
 <a href="PLF.MoreStlc.html#STLCExtended.T_App">STLCExtended.T_App</a> [in <a href="PLF.MoreStlc.html">PLF.MoreStlc</a>]<br/>
@@ -3556,8 +3556,8 @@ <h1>Lemma Index</h1>
 <a href="PLF.Hoare2.html#square_simpler_dec_correct">square_simpler_dec_correct</a> [in <a href="PLF.Hoare2.html">PLF.Hoare2</a>]<br/>
 <a href="PLF.Smallstep.html#stack_step_deterministic">stack_step_deterministic</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Types.html#step_deterministic">step_deterministic</a> [in <a href="PLF.Types.html">PLF.Types</a>]<br/>
-<a href="PLF.Norm.html#step_deterministic">step_deterministic</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#step_deterministic">step_deterministic</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
+<a href="PLF.Norm.html#step_deterministic">step_deterministic</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#step_normalizing">step_normalizing</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Norm.html#step_preserves_halting">step_preserves_halting</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Norm.html#step_preserves_R">step_preserves_R</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
@@ -3799,10 +3799,10 @@ <h1>Inductive Index</h1>
 <a href="PLF.Smallstep.html#SimpleArith1.step">SimpleArith1.step</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Smallstep.html#stack_step">stack_step</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.RecordSub.html#step">step</a> [in <a href="PLF.RecordSub.html">PLF.RecordSub</a>]<br/>
-<a href="PLF.Smallstep.html#step">step</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.Norm.html#step">step</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Types.html#step">step</a> [in <a href="PLF.Types.html">PLF.Types</a>]<br/>
 <a href="PLF.Sub.html#step">step</a> [in <a href="PLF.Sub.html">PLF.Sub</a>]<br/>
+<a href="PLF.Smallstep.html#step">step</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
 <a href="PLF.StlcProp.html#STLCArith.tm">STLCArith.tm</a> [in <a href="PLF.StlcProp.html">PLF.StlcProp</a>]<br/>
 <a href="PLF.StlcProp.html#STLCArith.ty">STLCArith.ty</a> [in <a href="PLF.StlcProp.html">PLF.StlcProp</a>]<br/>
 <a href="PLF.Records.html#STLCExtendedRecords.appears_free_in">STLCExtendedRecords.appears_free_in</a> [in <a href="PLF.Records.html">PLF.Records</a>]<br/>
@@ -3861,8 +3861,8 @@ <h1>Inductive Index</h1>
 <br/><br/><a name="inductive_V"></a><h2>V </h2>
 <a href="PLF.RecordSub.html#value">value</a> [in <a href="PLF.RecordSub.html">PLF.RecordSub</a>]<br/>
 <a href="PLF.Sub.html#value">value</a> [in <a href="PLF.Sub.html">PLF.Sub</a>]<br/>
-<a href="PLF.Norm.html#value">value</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Smallstep.html#value">value</a> [in <a href="PLF.Smallstep.html">PLF.Smallstep</a>]<br/>
+<a href="PLF.Norm.html#value">value</a> [in <a href="PLF.Norm.html">PLF.Norm</a>]<br/>
 <a href="PLF.Equiv.html#var_not_used_in_aexp">var_not_used_in_aexp</a> [in <a href="PLF.Equiv.html">PLF.Equiv</a>]<br/>
 <br/><br/><a name="inductive_W"></a><h2>W </h2>
 <a href="PLF.RecordSub.html#well_formed_ty">well_formed_ty</a> [in <a href="PLF.RecordSub.html">PLF.RecordSub</a>]<br/>

diff --git a/plf-current/index.html b/plf-current/index.html
@@ -82,7 +82,7 @@
 <div class="button"><a href="plf.tgz">下载</a></div>
 </div>
 
-<p>版本 5.6 (19 Nov 2018, Coq 8.8.0)</p>
+<p>版本 5.6 (07 Dec 2018, Coq 8.8.0)</p>
 </div>
 
 </div>

diff --git a/plf-current/plf.tgz b/plf-current/plf.tgz
diff --git a/plf-current/toc.html b/plf-current/toc.html
@@ -311,7 +311,7 @@ <h2><a href="Smallstep.html">小步操作语义&nbsp;&nbsp;&nbsp;&nbsp;(<b>Small
 </div>
 
 </li>
-<li><a href="Smallstep.html#lab148">多步规约</a>
+<li><a href="Smallstep.html#lab148">多步归约</a>
 <div>
 <ul class="doclist">
 <li><a href="Smallstep.html#lab149">例子</a>
@@ -486,48 +486,48 @@ <h2><a href="StlcProp.html">Properties of STLC&nbsp;&nbsp;&nbsp;&nbsp;(<b>StlcPr
 </li>
 </ul>
 </div>
-<h2><a href="MoreStlc.html">More on the Simply Typed Lambda-Calculus&nbsp;&nbsp;&nbsp;&nbsp;(<b>MoreStlc</b>)</a></h2>
+<h2><a href="MoreStlc.html">扩展简单类型 Lambda-演算&nbsp;&nbsp;&nbsp;&nbsp;(<b>MoreStlc</b>)</a></h2>
 <div>
 <ul class="doclist">
 <li><a href="MoreStlc.html">页首</a>
-<li><a href="MoreStlc.html#lab245">Simple Extensions to STLC</a>
+<li><a href="MoreStlc.html#lab245">STLC 的简单扩展</a>
 <div>
 <ul class="doclist">
-<li><a href="MoreStlc.html#lab246">Numbers</a>
+<li><a href="MoreStlc.html#lab246">数值</a>
 
 </li>
-<li><a href="MoreStlc.html#lab247">Let Bindings</a>
+<li><a href="MoreStlc.html#lab247">Let 绑定</a>
 
 </li>
-<li><a href="MoreStlc.html#lab248">Pairs</a>
+<li><a href="MoreStlc.html#lab248">二元组</a>
 
 </li>
-<li><a href="MoreStlc.html#lab249">Unit</a>
+<li><a href="MoreStlc.html#lab249">单元素类型</a>
 
 </li>
-<li><a href="MoreStlc.html#lab250">Sums</a>
+<li><a href="MoreStlc.html#lab250">和类型</a>
 
 </li>
-<li><a href="MoreStlc.html#lab251">Lists</a>
+<li><a href="MoreStlc.html#lab251">列表</a>
 
 </li>
-<li><a href="MoreStlc.html#lab252">General Recursion</a>
+<li><a href="MoreStlc.html#lab252">一般递归</a>
 
 </li>
-<li><a href="MoreStlc.html#lab255">Records</a>
+<li><a href="MoreStlc.html#lab255">字段组</a>
 
 </li>
 </ul>
 </div>
 
 </li>
-<li><a href="MoreStlc.html#lab258">Exercise: Formalizing the Extensions</a>
+<li><a href="MoreStlc.html#lab258">练习：形式化以上扩展</a>
 <div>
 <ul class="doclist">
-<li><a href="MoreStlc.html#lab264">Examples</a>
+<li><a href="MoreStlc.html#lab264">例子</a>
 
 </li>
-<li><a href="MoreStlc.html#lab272">Properties of Typing</a>
+<li><a href="MoreStlc.html#lab272">定型的性质</a>
 
 </li>
 </ul>

diff --git a/qc-current/index.html b/qc-current/index.html
@@ -42,7 +42,7 @@
             <div class="button"><a href="toc.html">阅读</a></div><br />
             <div class="button"><a href="qc.tgz">下载</a></div>
           </div>
-          <p>版本 1.0 (19 Nov 2018, Coq 8.8.0)</p>
+          <p>版本 1.0 (07 Dec 2018, Coq 8.8.0)</p>
         </div>
       </div>
     </div>

diff --git a/qc-current/qc.tgz b/qc-current/qc.tgz
diff --git a/vfa-current/index.html b/vfa-current/index.html
@@ -43,7 +43,7 @@
             <div class="button"><a href="vfa.tgz">Download</a></div>
           </div>
 
-          <p>Version 1.4 (19 Nov 2018, Coq 8.8.0)</p>
+          <p>Version 1.4 (07 Dec 2018, Coq 8.8.0)</p>
         </div>
 
       </div>

diff --git a/vfa-current/vfa.tgz b/vfa-current/vfa.tgz
-Original file line number
+Diff line change
@@ Expand Up / @@ -82,7 +82,7 @@ @@
     <div class="button"><a href="plf.tgz">下载</a></div>
     </div>
-    <p>版本 5.6 (19 Nov 2018, Coq 8.8.0)</p>
+    <p>版本 5.6 (07 Dec 2018, Coq 8.8.0)</p>
     </div>
     </div>
@@ Expand Down @@