Fixes to make develop compile

4 files changed, 6 insertions, 8 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 66170bc..eb2ddda 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -559,7 +559,7 @@ Definition transl_program (p: RTL.program) : Errors.res HTL.program :=
                              (fun i v => Errors.OK v) p.
 *)
 
-Definition main_is_internal {A B : Type} (p : AST.program A B) : bool :=
+Definition main_is_internal (p : RTL.program) : bool :=
   let ge := Globalenvs.Genv.globalenv p in
   match Globalenvs.Genv.find_symbol ge p.(AST.prog_main) with
   | Some b =>
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v
index 9b59269..724ac0a 100644
--- a/src/translation/HTLgenproof.v
+++ b/src/translation/HTLgenproof.v
@@ -393,7 +393,7 @@ Section CORRECTNESS.
       2: { reflexivity. }
       rewrite AssocMap.gss.
       unfold Verilog.merge_arr.
-      setoid_rewrite H1.
+      setoid_rewrite H3.
       reflexivity.
 
       rewrite combine_length.
diff --git a/src/translation/HTLgenspec.v b/src/translation/HTLgenspec.v
index 7d89a76..c617174 100644
--- a/src/translation/HTLgenspec.v
+++ b/src/translation/HTLgenspec.v
@@ -140,7 +140,7 @@ Inductive tr_instr (fin rtrn st stk : reg) : RTL.instruction -> stmnt -> stmnt -
     forall mem addr args s s' i c src n,
       translate_arr_access mem addr args stk s = OK c s' i ->
       tr_instr fin rtrn st stk (RTL.Istore mem addr args src n) (Vnonblock c (Vvar src))
-               (state_goto st n).
+               (state_goto st n)
 | tr_instr_Ijumptable :
     forall cexpr tbl r,
     cexpr = tbl_to_case_expr st tbl ->
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index bde98b8..52a87e3 100644
--- a/src/verilog/Value.v
+++ b/src/verilog/Value.v
@@ -372,7 +372,7 @@ Lemma boolToValue_ValueToBool :
   valueToBool (boolToValue 32 b) = b.
 Proof. destruct b; unfold valueToBool, boolToValue; simpl; trivial. Qed.
 
-Lemma ZToValue_valueToNat :
+(*Lemma ZToValue_valueToNat :
   forall x sz,
   sz > 0 ->
   (x < 2^(Z.of_nat sz))%Z ->
@@ -384,7 +384,5 @@ Proof.
     unfold Z.of_nat in *. destruct sz eqn:?. omega. simpl in H0.
     rewrite <- Pos2Z.inj_pow_pos in H0. Search (Z.pos _ < Z.pos _)%Z.
     Search Pos.to_nat (_ < _). (* Pos2Nat.inj_lt *)
-    Search Pos.to_nat.
-    (* Pos2Nat.is_succ: forall p : positive, exists n : nat, Pos.to_nat p = S n *)
-    Search S Pos.to_nat. Search (_ < _ <-> _)%positive. assert (exists p, Pos.to_nat p = S n).
-    econstructor. Search Pos2Nat.is_succ. Search Pos.of_succ_nat.
+    Search "inj" positive nat.
+*)