Use (new) bool2val instead of Val.of_bool

This P.R. implements the suggestion in issue #625.
It's an experiment, as in some cases it breaks existing VST proofs
at `forward_if` and related tactics.  The changes required in those
proofs are generally positive (simplifies proof scripts).
See further discussion at #625.  closes #625

Incidentally and unrelated:  closes #660

floyd/client_lemmas.v

@@ -1842,7 +1842,7 @@ Qed.
 Lemma typed_false_of_bool':
  forall x (P: Prop),
     ((x=false) -> P) ->
-    (typed_false tint (Val.of_bool x) -> P).
+    (typed_false tint (bool2val x) -> P).
 Proof.
 intuition.
 apply H, typed_false_of_bool; auto.
@@ -1851,7 +1851,7 @@ Qed.
 Lemma typed_true_of_bool':
  forall x (P: Prop),
     ((x=true) -> P) ->
-    (typed_true tint (Val.of_bool x) -> P).
+    (typed_true tint (bool2val x) -> P).
 Proof.
 intuition.
 apply H, typed_true_of_bool; auto.
@@ -1881,9 +1881,9 @@ Ltac intro_if_new :=
           let H := fresh "P" x in intro H
   | |- is_pointer_or_null ?x =>
           let H := fresh "PN" x in intro H
-  | |- typed_false _ (Val.of_bool _) -> _ =>
+  | |- typed_false _ (bool2val _) -> _ =>
           simple apply typed_false_of_bool'
-  | |- typed_true _ (Val.of_bool _) -> _ =>
+  | |- typed_true _ (bool2val _) -> _ =>
           simple apply typed_true_of_bool'
   | |- ptr_eq _ _ -> _ =>
           apply ptr_eq_e'

floyd/compare_lemmas.v

@@ -53,14 +53,16 @@ intros.
  apply prop_derives; intro.
  unfold tptr in H; simpl in H. unfold sem_binary_operation' in H.
  simpl in H. rewrite !andb_false_r in H.
- destruct (v rho); inv H.
- unfold sem_cmp_pp, strict_bool_val, nullval in *.
- destruct Archi.ptr64  eqn:Hp; simpl in H1;
- try solve [inv H1];
- try solve [pose proof (Int64.eq_spec i Int64.zero);
-                destruct (Int64.eq i Int64.zero); inv H1; auto];
- try solve [pose proof (Int.eq_spec i Int.zero);
-                destruct (Int.eq i Int.zero); inv H1; auto].
+ simpl in H.
+ red in H.
+ forget (v rho) as x. clear - H.
+ unfold sem_cmp_pp, strict_bool_val, nullval in *; simpl in *.
+ destruct Archi.ptr64; simpl in H;
+ destruct x; inv H.
+ - pose proof (Int64.eq_spec i Int64.zero);
+                destruct (Int64.eq i Int64.zero); inv H1; auto.
+ - pose proof (Int.eq_spec i Int.zero);
+                destruct (Int.eq i Int.zero); inv H1; auto.
 Qed.
 
 Definition  binary_operation_to_comparison (op: Cop.binary_operation) :=