r4166

Author: liyishuai

lf-current/AltAuto.html

@@ -2410,7 +2410,7 @@ <h1 class="libtitle">AltAuto<span class="subtitle">A Streamlined Treatment of Au
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/AltAuto.v

@@ -1825,4 +1825,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
 
     - Ltac functions and [match goal] *)
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:46 *)

lf-current/AltAutoTest.v

@@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
 idtac "MANUAL".
 Abort.
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:46 *)

lf-current/Auto.html

@@ -910,7 +910,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
 <span class="id" title="keyword">Proof</span>.<br/>
 &nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">P</span> <span class="id" title="var">Q</span> <span class="id" title="var">HP</span> <span class="id" title="var">HQ</span>. <span class="id" title="tactic">destruct</span> <span class="id" title="var">HP</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">y</span> <span class="id" title="var">HP'</span>]. <span class="id" title="tactic">eauto</span>.<br/>
 <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
-<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
 </div>
 </div>
 

lf-current/Auto.v

@@ -740,4 +740,4 @@ Proof.
   intros P Q HP HQ. destruct HP as [y HP']. eauto.
 Qed.
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:46 *)

lf-current/AutoTest.v

@@ -63,4 +63,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:46 *)

lf-current/Basics.html

@@ -2691,7 +2691,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Coq<
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-04-23&nbsp;03:45&nbsp;*)</span><br/>
 </div>
 </div>
 

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.  *)
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:45 *)

lf-current/BasicsTest.v

@@ -521,4 +521,4 @@ idtac "".
 idtac "********** Advanced **********".
 Abort.
 
-(* 2023-12-24 12:53 *)
+(* 2024-04-23 03:46 *)

lf-current/Bib.html

@@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
 </div>
 <div class="code">
 
-<span class="comment">(*&nbsp;2023-12-24&nbsp;12:53&nbsp;*)</span><br/>
+<span class="comment">(*&nbsp;2024-04-23&nbsp;03:46&nbsp;*)</span><br/>
 </div>
 </div>