From 7707396c5010d88c3d0be6ecee816d8da7ed0ee0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 16 Feb 2017 21:55:14 +0100
Subject: Fixing #5339 (anomaly with 'pat in record parameters).

---
 toplevel/record.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/toplevel/record.ml b/toplevel/record.ml
index b8dcf81fde..8d35e5a3da 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -108,7 +108,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
       List.iter 
 	(function LocalRawDef (b, _) -> error default_binder_kind b
 	   | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | LocalPattern _ -> assert false) ps
+           | LocalPattern (loc,_,_) ->
+              Loc.raise loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps
   in 
   let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in
   let t', template = match t with 
-- 
cgit v1.2.3