diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 10:09:34 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-03-01 10:09:34 +0000 |
| commit | bb7d7482724489521dde94a5b70af7864acfa802 (patch) | |
| tree | 821dfa6baa108de2b2af016e842164f01a39101f /pretyping/pattern.ml | |
| parent | 05b756a9a5079e91c5015239bb801918d4903c08 (diff) | |
nouvelle implantation de la reduction
suppression de IsXtra du noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pattern.ml')
| -rw-r--r-- | pretyping/pattern.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index 625e28d56..b83019b45 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -269,7 +269,7 @@ let rec sub_match nocc pat c = let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))) | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _ - | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ -> + | IsRel _|IsMeta _|IsVar _|IsSort _ -> (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with | PatternMatchingFailure -> raise (NextOccurrence nocc) | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1))) @@ -320,7 +320,6 @@ let rec pattern_of_constr t = | IsFix f -> PFix f | IsCoFix _ -> error "pattern_of_constr: (co)fix currently not supported" - | IsXtra _ -> anomaly "No longer supported" and pattern_of_ref ref inst = let args = Declare.extract_instance ref inst in |