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 Co-authored-by: Gaëtan Gilbert --- kernel/entries.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'kernel/entries.ml') diff --git a/kernel/entries.ml b/kernel/entries.ml index e0b678621a..ae64112e33 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -91,8 +91,7 @@ type parameter_entry = Id.Set.t option * types in_universes_entry * inline type primitive_entry = { - prim_entry_type : types option; - prim_entry_univs : Univ.ContextSet.t; (* always monomorphic *) + prim_entry_type : types in_universes_entry option; prim_entry_content : CPrimitives.op_or_type; } -- cgit v1.2.3