From 70930579d8454a4ff50ee0ea1e97a55863bf01f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:14 +0200
Subject: More explicit message when a {struct x} argument refers to a local
 definition.

---
 interp/topconstr.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 89e04b69d2..513fa8f161 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -176,7 +176,12 @@ let split_at_annot bl na =
               in
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
+	| CLocalDef ((_,na),_,_) as x :: rest ->
+           if Name.equal (Name id) na then
+             user_err ~loc
+               (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+           else
+             aux (x :: acc) rest
         | CLocalPattern (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
-- 
cgit v1.2.3