From 3fdb62dee9830bb551798ee9c3dd2a3af1493e8d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 26 Oct 2018 16:55:54 +0200
Subject: Error when [foo.(bar)] is used with nonprojection [bar]

(warn if bar is a nonprimitive projection)
---
 pretyping/recordops.ml  | 2 ++
 pretyping/recordops.mli | 2 ++
 2 files changed, 4 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 6d9e3230a4..fc355c2c79 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -103,6 +103,8 @@ let find_projection = function
   | ConstRef cst -> Cmap.find cst !projection_table
   | _ -> raise Not_found
 
+let is_projection cst = Cmap.mem cst !projection_table
+
 let prim_table =
   Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3e43372b65..76d36c9b62 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -44,6 +44,8 @@ val find_projection_nparams : GlobRef.t -> int
 (** raise [Not_found] if not a projection *)
 val find_projection : GlobRef.t -> struc_typ
 
+val is_projection : Constant.t -> bool
+
 (** Sets up the mapping from constants to primitive projections *)
 val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
-- 
cgit v1.2.3