diff options
| author | herbelin | 2000-09-10 20:37:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-10 20:37:37 +0000 |
| commit | e72024e2292a50684b7f280d6efb8fee090e2dbf (patch) | |
| tree | fdba2d8c55f0c74aee8800a0e8c9aec3d3b8a584 /parsing/pattern.ml | |
| parent | 583992b6ce38655855f6625a26046ce84c53cdc1 (diff) | |
Suppression de Abst
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/pattern.ml')
| -rw-r--r-- | parsing/pattern.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/parsing/pattern.ml b/parsing/pattern.ml index ff747d4e35..17a4535a4d 100644 --- a/parsing/pattern.ml +++ b/parsing/pattern.ml @@ -53,7 +53,6 @@ let label_of_ref = function | RInd (sp,_) -> IndNode sp | RConstruct (sp,_) -> CstrNode sp | RVar id -> VarNode id - | RAbst _ -> error "Obsolète" | REVar _ -> raise BoundPattern let rec head_pattern_bound t = @@ -265,12 +264,12 @@ let rec sub_match nocc pat c = (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with | PatternMatchingFailure -> let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in - (lm,mkMutCase (ci,hd,List.hd le,List.tl le)) + (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)) | NextOccurrence nocc -> let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in - (lm,mkMutCase (ci,hd,List.hd le,List.tl le))) + (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))) | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _ - | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _|IsAbst (_, _) -> + | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ -> (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) @@ -327,4 +326,4 @@ let rec pattern_of_constr t = Array.map pattern_of_constr br) | IsFix _ | IsCoFix _ -> error "pattern_of_constr: (co)fix currently not supported" - | IsAbst _ | IsXtra _ -> anomaly "No longer supported" + | IsXtra _ -> anomaly "No longer supported" |