Fix Array.empty precompilation (#25)

Fix #24

Author: SkySkimmer

src/tac2compiledPrim.ml

@@ -43,9 +43,8 @@ let define name arity f =
   registered := (name,arity) :: !registered;
   f
 
-(* Adds a thunk *)
 let define0 name v =
-  define name 1 (fun (_:valexpr) -> v)
+  define name 0 v
 
 let define1 name r0 f =
   define name 1 (fun x0 -> f (repr_to r0 x0))
@@ -56,7 +55,7 @@ let define2 name r0 r1 f =
 let define3 name r0 r1 r2 f =
   define name 3 (fun x0 x1 x2 -> f (repr_to r0 x0) (repr_to r1 x1) (repr_to r2 x2))
 
-let array_empty = define0 "array_empty" (return (ValBlk (0, [||])))
+let array_empty = define0 "array_empty" (ValBlk (0, [||]))
 
 let array_make = define2 "array_make" int valexpr begin fun n x ->
   if n < 0 || n > Sys.max_array_length then throw err_outofbounds

src/tac2compiledPrim.mli

@@ -11,7 +11,7 @@
 open Ltac2_plugin.Tac2val
 open Proofview
 
-val array_empty : valexpr -> valexpr tactic
+val array_empty : valexpr
 val array_make : valexpr -> valexpr -> valexpr tactic
 val array_length : valexpr -> valexpr tactic
 val array_set : valexpr -> valexpr -> valexpr -> valexpr tactic

tests/_CoqProject

@@ -11,6 +11,7 @@ compiler_bug_6.v
 compiler_bug_14.v
 compiler_bug_16.v
 compiler_bug_17.v
+compiler_bug_24.v
 
 -I src
 

tests/compiler_bug_24.v

@@ -0,0 +1,6 @@
+Require Import Ltac2Compiler.Ltac2Compiler.
+From Ltac2 Require Import Array.
+Ltac2 test () := Array.empty.
+Ltac2 Eval Array.length (test ()).
+Ltac2 Compile Array.empty.
+Ltac2 Eval Array.length (test ()).