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 --- plugins/ssrmatching/ssrmatching.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'plugins/ssrmatching') diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 1ed632f03f..5dedae6388 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -312,6 +312,7 @@ let iter_constr_LR f c = match kind c with | Fix (_, (_, t, b)) | CoFix (_, (_, t, b)) -> for i = 0 to Array.length t - 1 do f t.(i); f b.(i) done | Proj(_,a) -> f a + | Array(_u,t,def,ty) -> Array.iter f t; f def; f ty | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ | Int _ | Float _) -> () -- cgit v1.2.3