From db294322a9ae8954d5325ad0f02e37bf0db70548 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 22 Apr 2015 18:50:05 +0200
Subject: Fixing non exhaustive pattern-matching.

---
 pretyping/patternops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a766b1265e..fb629d049f 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -395,7 +395,7 @@ 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))
-        | (None | Some (GHole _)), None -> PMeta None
+        | (None | Some (GHole _)), _ -> PMeta None
 	| Some p, None ->
             user_err_loc (loc,"",strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
-- 
cgit v1.2.3