From 0ea2d0ff4ed84e1cc544c958b8f6e98f6ba2e9b6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 3 Feb 2020 18:19:42 +0100
Subject: Primitive persistent arrays

Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.

Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
---
 kernel/cClosure.mli | 1 +
 1 file changed, 1 insertion(+)

(limited to 'kernel/cClosure.mli')

diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index c1e5f12df7..ada0fc9780 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -118,6 +118,7 @@ type fterm =
   | FEvar of existential * fconstr subs
   | FInt of Uint63.t
   | FFloat of Float64.t
+  | FArray of Univ.Instance.t * fconstr Parray.t * fconstr
   | FLIFT of int * fconstr
   | FCLOS of constr * fconstr subs
   | FLOCKED
-- 
cgit v1.2.3