search

SkySkimmer / coq-ltac2-compiler

GNU Lesser General Public License v2.1
5 stars 0 forks source link

Incorrect compilation of Array.empty #24

Closed SkySkimmer closed 5 months ago

SkySkimmer commented 5 months ago 
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 ()). (* Fails with anomaly in `Tac2ffi.to_array` *)

reported by @janno