diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constrMatching.ml (renamed from pretyping/matching.ml) | 3 | ||||
| -rw-r--r-- | pretyping/constrMatching.mli (renamed from pretyping/matching.mli) | 0 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 10 |
4 files changed, 7 insertions, 8 deletions
diff --git a/pretyping/matching.ml b/pretyping/constrMatching.ml index 0d3f24928..45b097c00 100644 --- a/pretyping/matching.ml +++ b/pretyping/constrMatching.ml @@ -219,7 +219,7 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = let s' = List.fold_left (fun l (na,_,t) -> (Anonymous,na,t)::l) stk ctx' in let b1 = lift_pattern n b1 and b1' = lift_pattern n' b1' in - sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2' + sorec s' (sorec s (sorec stk subst a1 a2) b1 b2) b1' b2' else raise PatternMatchingFailure @@ -407,4 +407,3 @@ let matches_conv env sigma c p = let is_matching_conv env sigma pat n = try let _ = matches_conv env sigma pat n in true with PatternMatchingFailure -> false - diff --git a/pretyping/matching.mli b/pretyping/constrMatching.mli index b82f11525..b82f11525 100644 --- a/pretyping/matching.mli +++ b/pretyping/constrMatching.mli diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d4892f2f8..469be6d9e 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -20,7 +20,7 @@ Miscops Glob_ops Redops Patternops -Matching +ConstrMatching Tacred Typeclasses_errors Typeclasses diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 46037e5ee..4b03c935f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -22,7 +22,6 @@ open Closure open Reductionops open Cbv open Patternops -open Matching open Locus (* Errors *) @@ -804,8 +803,8 @@ let simpl env sigma c = strong whd_simpl env sigma c let matches_head c t = match kind_of_term t with - | App (f,_) -> matches c f - | _ -> raise PatternMatchingFailure + | App (f,_) -> ConstrMatching.matches c f + | _ -> raise ConstrMatching.PatternMatchingFailure let contextually byhead (occs,c) f env sigma t = let (nowhere_except_in,locs) = Locusops.convert_occs occs in @@ -815,7 +814,8 @@ let contextually byhead (occs,c) f env sigma t = if nowhere_except_in && (!pos > maxocc) then t else try - let subst = if byhead then matches_head c t else matches c t in + let subst = + if byhead then matches_head c t else ConstrMatching.matches c t in let ok = if nowhere_except_in then Int.List.mem !pos locs else not (Int.List.mem !pos locs) in @@ -829,7 +829,7 @@ let contextually byhead (occs,c) f env sigma t = mkApp (f, Array.map_left (traverse envc) l) else t - with PatternMatchingFailure -> + with ConstrMatching.PatternMatchingFailure -> map_constr_with_binders_left_to_right (fun d (env,c) -> (push_rel d env,lift_pattern 1 c)) traverse envc t |