Merge branch 'trunk' into located_switch

1 files changed, 7 insertions, 2 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index eb89b2ef24..4ffb7020f3 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -179,8 +179,13 @@ let split_at_annot bl na =
               in
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
-        | CLocalPattern (loc,_) :: 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 (_,_) :: rest ->
             Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ?loc