diff --git a/src/tac2compiledPrim.ml b/src/tac2compiledPrim.ml index f41b1f7..b7e2fea 100644 --- a/src/tac2compiledPrim.ml +++ b/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 diff --git a/src/tac2compiledPrim.mli b/src/tac2compiledPrim.mli index faf915d..cf718be 100644 --- a/src/tac2compiledPrim.mli +++ b/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 diff --git a/tests/compiler_bug_24.v b/tests/compiler_bug_24.v new file mode 100644 index 0000000..723809e --- /dev/null +++ b/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 ()).