From 3971466fbdd9aa1883a4468de3d67fdf90fee02d Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 13 Aug 2020 23:22:20 +0100
Subject: Add html generation and clean Coq files

---
 Makefile                      | 5 +++++
 src/translation/HTLgenproof.v | 3 +--
 src/verilog/Array.v           | 2 +-
 src/verilog/Value.v           | 4 +---
 src/verilog/ValueInt.v        | 1 -
 5 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/Makefile b/Makefile
index 518d4c9..dce965d 100644
--- a/Makefile
+++ b/Makefile
@@ -17,6 +17,8 @@ COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \
 COQEXEC := $(COQBIN)coqtop $(COQINCLUDES) -batch -load-vernac-source
 COQMAKE := $(COQBIN)coq_makefile
 
+COQDOCFLAGS := --no-lib-name
+
 VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
 
 PREFIX ?= .
@@ -41,6 +43,9 @@ proof: Makefile.coq
 	$(MAKE) -f Makefile.coq
 	@rm -f src/extraction/STAMP
 
+doc: Makefile.coq
+	$(MAKE) COQDOCFLAGS="$(COQDOCFLAGS)" -f Makefile.coq html
+
 extraction: src/extraction/STAMP
 
 test:
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 403a97f..bf63800 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -753,7 +753,6 @@ Section CORRECTNESS.
     - rewrite H0 in Heqb. rewrite H1 in Heqb. discriminate.
     - rewrite Heqb in Heqb0. discriminate.
     (*- unfold Int.ror. unfold Int.or. unfold Int.shru, Int.shl, Int.sub. unfold intToValue. unfold Int.modu,
-      Search Int.repr.
       repeat (rewrite Int.unsigned_repr). auto.*)
     - unfold Op.eval_addressing32 in *. repeat (unfold_match H2); inv H2.
       + unfold translate_eff_addressing in *. repeat (unfold_match H1).
@@ -1105,7 +1104,7 @@ Section CORRECTNESS.
       rewrite Ptrofs.unsigned_repr by (unfold_constants; lia).
       rewrite Int.unsigned_repr by (unfold_constants; lia).
 
-      unfold Ptrofs.of_int. Search Int.add. rewrite Int.add_commut.
+      unfold Ptrofs.of_int. rewrite Int.add_commut.
       pose proof Integers.Ptrofs.agree32_add as AGR. unfold Ptrofs.agree32 in *.
       erewrite AGR.
       3: { unfold uvalueToZ. rewrite Ptrofs.unsigned_repr. trivial. apply Int.unsigned_range_2. }
diff --git a/src/verilog/Array.v b/src/verilog/Array.v
index 02b6d33..fe0f6b2 100644
--- a/src/verilog/Array.v
+++ b/src/verilog/Array.v
@@ -156,7 +156,7 @@ Proof.
   intros.
 
   unfold array_get.
-  info_eauto with array.
+  eauto with array.
 Qed.
 
 Lemma array_get_get_error {A : Type} :
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index 41a41b4..d6a3d8b 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -40,8 +40,6 @@ Record value : Type :=
     vword: word vsize
   }.
 
-Search N.of_nat.
-
 (** ** Value conversions
 
 Various conversions to different number types such as [N], [Z], [positive] and
@@ -490,7 +488,7 @@ Qed.
 Proof.
   intros. unfold Int.add, valueToInt, intToValue. repeat (rewrite Int.unsigned_repr).
   rewrite (@vadd_vplus v1 v2 EQ). trivial.
-  unfold uvalueToZ. Search word "bound". pose proof (@uwordToZ_bound (vsize v2) (vword v2)).
+  unfold uvalueToZ. pose proof (@uwordToZ_bound (vsize v2) (vword v2)).
   rewrite H in EQ. rewrite <- EQ in H0 at 3.*)
   (*rewrite zadd_vplus3. trivia*)
 
diff --git a/src/verilog/ValueInt.v b/src/verilog/ValueInt.v
index 2220998..f1fd056 100644
--- a/src/verilog/ValueInt.v
+++ b/src/verilog/ValueInt.v
@@ -77,7 +77,6 @@ Definition ptrToValue (i : ptrofs) : value := Ptrofs.to_int i.
 Definition valueToPtr (i : value) : Integers.ptrofs :=
   Ptrofs.of_int i.
 
-Search Ptrofs.of_int Ptrofs.to_int.
 Definition valToValue (v : Values.val) : option value :=
   match v with
   | Values.Vint i => Some (intToValue i)
-- 
cgit