Skip to content

Commit 350f905

Browse files
catalin-hritcucatalin-hritcu
committed
r4304
1 parent f2b2568 commit 350f905

File tree

341 files changed

+4697
-3181
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

341 files changed

+4697
-3181
lines changed

‎lf-current/AltAuto.html‎

Lines changed: 41 additions & 41 deletions
Large diffs are not rendered by default.

‎lf-current/AltAuto.v‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -66,7 +66,7 @@ Proof.
6666
induction M
6767
as [| x'
6868
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
69-
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
69+
| s1 re1 re2 Hmatch IH | s2 re1 re2 Hmatch IH
7070
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
7171
- (* MEmpty *) simpl. apply MEmpty.
7272
- (* MChar *) simpl. apply MChar.
@@ -212,7 +212,7 @@ Proof.
212212
induction M
213213
as [| x'
214214
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
215-
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
215+
| s1 re1 re2 Hmatch IH | s2 re1 re2 Hmatch IH
216216
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
217217
(* Do the [simpl] for every case here: *)
218218
simpl.
@@ -298,7 +298,7 @@ Proof.
298298
induction M
299299
as [| x'
300300
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
301-
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
301+
| s1 re1 re2 Hmatch IH | s2 re1 re2 Hmatch IH
302302
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2];
303303
(* Do the [simpl] for every case here: *)
304304
simpl.
@@ -390,7 +390,7 @@ Proof.
390390
induction M
391391
as [| x'
392392
| s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
393-
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
393+
| s1 re1 re2 Hmatch IH | s2 re1 re2 Hmatch IH
394394
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
395395
- (* MEmpty *) simpl. apply MEmpty.
396396
- (* MChar *) simpl. apply MChar.
@@ -1183,7 +1183,7 @@ Proof.
11831183
intros T re s Hmatch.
11841184
induction Hmatch
11851185
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
1186-
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
1186+
| s1 re1 re2 Hmatch IH | s2 re1 re2 Hmatch IH
11871187
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ];
11881188
simpl; try lia;
11891189
intros Hlen.
@@ -1832,4 +1832,4 @@ Definition manual_grade_for_nor_intuition : option (nat*string) := None.
18321832
18331833
- Ltac functions and [match goal] *)
18341834

1835-
(* 2024-12-26 02:02 *)
1835+
(* 2024-12-26 15:02 *)

‎lf-current/AltAutoTest.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -255,4 +255,4 @@ idtac "---------- nor_intuition ---------".
255255
idtac "MANUAL".
256256
Abort.
257257

258-
(* 2024-12-26 02:03 *)
258+
(* 2024-12-26 15:03 *)

‎lf-current/Auto.html‎

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -105,7 +105,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
105105
</div>
106106

107107
<div class="doc">
108-
<a id="lab441"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">auto</span></span> Tactic</h1>
108+
<a id="lab452"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">auto</span></span> Tactic</h1>
109109

110110
<div class="paragraph"> </div>
111111

@@ -390,7 +390,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
390390
</div>
391391

392392
<div class="doc">
393-
<a id="lab442"></a><h1 class="section">Searching For Hypotheses</h1>
393+
<a id="lab453"></a><h1 class="section">Searching For Hypotheses</h1>
394394

395395
<div class="paragraph"> </div>
396396

@@ -673,7 +673,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
673673
your proofs, both to avoid tedium and to "future proof" them.
674674
<div class="paragraph"> </div>
675675

676-
<a id="lab443"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> and <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> tactics</h1>
676+
<a id="lab454"></a><h1 class="section">The <span class="inlinecode"><span class="id" title="tactic">eapply</span></span> and <span class="inlinecode"><span class="id" title="tactic">eauto</span></span> tactics</h1>
677677

678678
<div class="paragraph"> </div>
679679

@@ -804,7 +804,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
804804
ordinary variants don't do the job.
805805
<div class="paragraph"> </div>
806806

807-
<a id="lab444"></a><h1 class="section">Constraints on Existential Variables</h1>
807+
<a id="lab455"></a><h1 class="section">Constraints on Existential Variables</h1>
808808

809809
<div class="paragraph"> </div>
810810

@@ -910,7 +910,7 @@ <h1 class="libtitle">Auto<span class="subtitle">More Automation</span></h1>
910910
<span class="id" title="keyword">Proof</span>.<br/>
911911
&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/>
912912
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
913-
<span class="comment">(*&nbsp;2024-12-26&nbsp;02:02&nbsp;*)</span><br/>
913+
<span class="comment">(*&nbsp;2024-12-26&nbsp;15:02&nbsp;*)</span><br/>
914914
</div>
915915
</div>
916916

‎lf-current/Auto.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -740,4 +740,4 @@ Proof.
740740
intros P Q HP HQ. destruct HP as [y HP']. eauto.
741741
Qed.
742742

743-
(* 2024-12-26 02:02 *)
743+
(* 2024-12-26 15:02 *)

‎lf-current/AutoTest.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,4 +63,4 @@ idtac "".
6363
idtac "********** Advanced **********".
6464
Abort.
6565

66-
(* 2024-12-26 02:03 *)
66+
(* 2024-12-26 15:03 *)

‎lf-current/Basics.html‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2711,7 +2711,7 @@ <h1 class="libtitle">Basics<span class="subtitle">Functional Programming in Coq<
27112711
</div>
27122712
<div class="code">
27132713

2714-
<span class="comment">(*&nbsp;2024-12-26&nbsp;02:02&nbsp;*)</span><br/>
2714+
<span class="comment">(*&nbsp;2024-12-26&nbsp;15:02&nbsp;*)</span><br/>
27152715
</div>
27162716
</div>
27172717

‎lf-current/Basics.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2034,4 +2034,4 @@ Example test_bin_incr6 :
20342034
output. But since they have to be graded by a human, the test
20352035
script won't be able to tell you much about them. *)
20362036

2037-
(* 2024-12-26 02:02 *)
2037+
(* 2024-12-26 15:02 *)

‎lf-current/BasicsTest.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -519,4 +519,4 @@ idtac "".
519519
idtac "********** Advanced **********".
520520
Abort.
521521

522-
(* 2024-12-26 02:02 *)
522+
(* 2024-12-26 15:02 *)

‎lf-current/Bib.html‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
3636

3737
<div class="paragraph"> </div>
3838

39-
<a id="lab483"></a><h1 class="section">Resources cited in this volume</h1>
39+
<a id="lab494"></a><h1 class="section">Resources cited in this volume</h1>
4040

4141
<div class="paragraph"> </div>
4242

@@ -84,7 +84,7 @@ <h1 class="libtitle">Bib<span class="subtitle">Bibliography</span></h1>
8484
</div>
8585
<div class="code">
8686

87-
<span class="comment">(*&nbsp;2024-12-26&nbsp;02:02&nbsp;*)</span><br/>
87+
<span class="comment">(*&nbsp;2024-12-26&nbsp;15:02&nbsp;*)</span><br/>
8888
</div>
8989
</div>
9090

0 commit comments

Comments
 (0)