rocq-community · Casteran · Jul 13, 2023 · Jul 13, 2023 · Jul 26, 2023 · Jul 26, 2023
diff --git a/ch15_general_recursion/SRC/log2_function.v b/ch15_general_recursion/SRC/log2_function.v
@@ -83,7 +83,8 @@ Proof.
       intro H.
       case_eq (exp2 p).
       * intro H0; destruct (exp2_positive p);auto.
-      * intros n H0;  rewrite H0 in H; elimtype False; lia.   
+      * intros n H0;  rewrite H0 in H. assert (H1:False) by lia.  
+        destruct H1.
  - intros p H;  destruct p. 
    +  simpl in H;  subst n;    contradiction. 
    +  simpl in H; rewrite (IHn0 p); auto. 

diff --git a/ch16_proof_by_reflection/SRC/prime_sqrt.v b/ch16_proof_by_reflection/SRC/prime_sqrt.v
@@ -122,7 +122,7 @@ Theorem test_odds_correct :
 Proof.
  induction n.
  -  intros x p Hp1 H1ltx Hn q Hint.
-    elimtype False;  lia.
+    assert (FF: False) by lia; destruct FF.
   - intros x p Hp H1ltx; simpl (test_odds (S n) p (Z_of_nat x));
     intros Htest q (H1ltq, Hqle).
     case_eq (test_odds n (p -2) (Z_of_nat x)).

diff --git a/doc/typeClassesTut/.gitignore b/doc/typeClassesTut/.gitignore
@@ -0,0 +1,6 @@
+*.pdf
+*.log
+*.aux
+*.blg
+*.out
+*.bbl
diff --git a/doc/typeClassesTut/Makefile b/doc/typeClassesTut/Makefile
@@ -0,0 +1,18 @@
+DEP_Files = typeclassestut.tex \
+	morebiblio.bib \
+	biblio.bib
+
+.PHONY:all
+all: typeclassestut.pdf
+
+typeclassestut.pdf: ${DEP_Files}
+	lualatex typeclassestut.tex
+	bibtex typeclassestut
+	lualatex typeclassestut.tex
+	lualatex typeclassestut.tex
+	lualatex typeclassestut.tex
+
+
+.PHONY:clean
+clean:
+	@${RM} typeclassestut.pdf *.aux *.ind   *.bbl *.blg *.log  *.out
-Original file line number
+Diff line change
@@ -0,0 +1,6 @@
+    *.pdf
+    *.log
+    *.aux
+    *.blg
+    *.out
+    *.bbl