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 ++
 1 file changed, 2 insertions(+)

(limited to 'pretyping/recordops.ml')

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"
 
-- 
cgit v1.2.3