From 7d243d68abf11feeb7a6c421fb75505205938a80 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 2 May 2000 17:16:33 +0000
Subject: pattern-matching non-exhaustif (occur_rawconstr)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@398 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b5b246f213..fd6a0457d3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -315,7 +315,7 @@ let occur_rawconstr id =
 	(array_exists occur tyl) or
 	(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
     | RCast (loc,c,t) -> (occur c) or (occur t)
-    | (RSort _ | RHole _ | RRef _ ) -> false
+    | (RSort _ | RHole _ | RRef _ | RMeta _) -> false
 
   and occur_pattern (idl,p,c) = not (List.mem id idl) & (occur c)
 
-- 
cgit v1.2.3