Commit 392c3249 authored by David Monniaux's avatar David Monniaux
Browse files

Merge remote-tracking branch 'origin/mppa-work' into RTLblock

parents fd8242e4 69f4580c
......@@ -424,7 +424,7 @@ Qed.
(*
Lemma signed_0_eqb :
forall x, (Z.eqb (Int.signed x) 0) = Int.eq x Int.zero.
Admitted.
Qed.
*)
Lemma Z_quot_le: forall a b,
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment