Merge remote-tracking branch 'origin/master' into named-externals

Conflicts:
	arm/TargetPrinter.ml
	backend/CMparser.mly
	backend/SelectLongproof.v
	backend/Selectionproof.v
	cfrontend/C2C.ml
	checklink/Asm_printers.ml
	checklink/Check.ml
	checklink/Fuzz.ml
	common/AST.v
	debug/DebugInformation.ml
	debug/DebugInit.ml
	debug/DwarfPrinter.ml
	debug/DwarfTypes.mli
	debug/Dwarfgen.ml
	exportclight/ExportClight.ml
	ia32/TargetPrinter.ml
	powerpc/Asm.v
	powerpc/SelectOpproof.v
	powerpc/TargetPrinter.ml

1 files changed, 9 insertions, 0 deletions

diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 6a027eee..4ad5e2f9 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -496,6 +496,15 @@ Definition transl_op
   | Ointoffloat, a1 :: nil =>
       do r1 <- freg_of a1; do r <- ireg_of res;
       OK (Pfcti r r1 :: k)
+  | Ointuoffloat, a1 :: nil =>
+      do r1 <- freg_of a1; do r <- ireg_of res;
+      OK (Pfctiu r r1 :: k)
+  | Ofloatofint, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- freg_of res;
+      OK (Pfcfi r r1 :: k)
+  | Ofloatofintu, a1 :: nil =>
+      do r1 <- ireg_of a1; do r <- freg_of res;
+      OK (Pfcfiu r r1 :: k)
   | Ofloatofwords, a1 :: a2 :: nil =>
       do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- freg_of res;
       OK (Pfmake r r1 r2 :: k)