Merge branch 'develop' into arrays-proof

2 files changed, 5 insertions, 9 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index dc82fb1..e637d6f 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -572,8 +572,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 := true.
-(*
+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 =>
@@ -582,7 +581,7 @@ Definition main_is_internal {A B : Type} (p : AST.program A B) : bool := true.
     | _ => false
     end
   | _ => false
-  end. *)
+  end.
 
 Definition transl_program (p : RTL.program) : Errors.res HTL.program :=
   if main_is_internal p
diff --git a/src/verilog/Value.v b/src/verilog/Value.v
index becc44c..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,8 +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.
-Admitted.
+    Search "inj" positive nat.
+*)