From 79e2ca7374ef8d8dc22c29d1d98ff71c4ad50f69 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 25 Dec 2000 23:45:50 +0000
Subject: bug head_pattern_bound

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1213 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/pattern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 43e5d4877c..3dd339d466 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -59,8 +59,8 @@ let rec head_pattern_bound t =
     | PCase (p,c,br)        -> head_pattern_bound c
     | PRef r                -> label_of_ref r
     | PVar id               -> VarNode id
-    | PRel _ | PMeta _ | PSoApp _  | PSort _ -> raise BoundPattern
-    | PBinder(BLambda,_,_,_) | PFix _ | PCoFix _ ->
+    | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ -> raise BoundPattern
+    | PBinder(BLambda,_,_,_) | PCoFix _ ->
       anomaly "head_pattern_bound: not a type"
 
 let head_of_constr_reference c = match kind_of_term c with
-- 
cgit v1.2.3