From 9fa7f38b74ec26f880d9ec983a5a1c8699e0a612 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 16:35:15 +0200
Subject: Fixing #3383 (a "return" clause without an "in" clause is not enough
 for being able to interpret a "match" as a constr pattern).

---
 pretyping/patternops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 705e594af1..a766b1265e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,9 @@ let rec pat_of_raw metas vars = function
 	| Some p, Some (_,_,nal) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-	| _ -> PMeta None
+        | (None | Some (GHole _)), None -> PMeta None
+	| Some p, None ->
+            user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
 	{ cip_style = sty;
-- 
cgit v1.2.3