From 6df2c6dc38c70954608981cb9d010468ff8a4224 Mon Sep 17 00:00:00 2001 From: nilfit <nils.fitinghoff@gmail.com> Date: Tue, 17 Jul 2018 18:18:50 +0200 Subject: [PATCH] unsafely fix extraction of list.Nth Extracted code now uses `List.nth_opt` instead of `nth`. Also changed to unsafely convert from `Z.t` to ocaml int. This is bad and doesn't work in general. --- drivers/ocaml64.drv | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/drivers/ocaml64.drv b/drivers/ocaml64.drv index d83f52fde..61b8a0d87 100644 --- a/drivers/ocaml64.drv +++ b/drivers/ocaml64.drv @@ -53,7 +53,7 @@ theory list.Mem end theory list.Nth - syntax function nth "List.nth %1 %2" + syntax function nth "List.nth_opt %2 (Z.to_int %1)" end theory list.Append -- GitLab