From 3ead22d31bedbd53842fe74e9d59d2413505e211 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Mon, 16 Apr 2018 13:45:25 +0200 Subject: [PATCH] extraction driver: use %1.(%2)<-%3 instead of Array.set otherwise, this is not optimized when compiling with -unsafe (similarly for Array.get) --- drivers/ocaml64.drv | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv index 08f5967fc..2f1a12db3 100644 --- a/drivers/ocaml64.drv +++ b/drivers/ocaml64.drv @@ -10,7 +10,7 @@ end module HighOrd syntax type (->) "%1 -> %2" - syntax val (@) "%1 %2" + syntax val ( @ ) "%1 %2" end theory option.Option @@ -351,8 +351,8 @@ module mach.array.Array63 syntax type array "(%1 array)" syntax val make "Array.make %1 %2" - syntax val ([]) "Array.get %1 %2" - syntax val ([]<-) "Array.set %1 %2 %3" + syntax val ([]) "%1.(%2)" + syntax val ([]<-) "%1.(%2) <- %3" syntax val length "Array.length %1" syntax val append "Array.append %1 %2" syntax val sub "Array.sub %1 %2 %3" -- GitLab