diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/matching.ml | 13 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 4 | ||||
| -rw-r--r-- | pretyping/patternops.mli | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 |
4 files changed, 10 insertions, 11 deletions
diff --git a/pretyping/matching.ml b/pretyping/matching.ml index 979a7dae3..65971d6e3 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -62,12 +62,12 @@ let warn_bound_again name = let constrain n (ids, m as x) (names, terms as subst) = try - let (ids', m') = List.assoc n terms in + let (ids', m') = Id.Map.find n terms in if List.equal Id.equal ids ids' && eq_constr m m' then subst else raise PatternMatchingFailure with Not_found -> let () = if Id.Map.mem n names then warn_bound_meta n in - (names, (n, x) :: terms) + (names, Id.Map.add n x terms) let add_binders na1 na2 (names, terms as subst) = match na1, na2 with | Name id1, Name id2 -> @@ -76,7 +76,7 @@ let add_binders na1 na2 (names, terms as subst) = match na1, na2 with (names, terms) else let names = Id.Map.add id1 id2 names in - let () = if List.mem_assoc id1 terms then warn_bound_again id1 in + let () = if Id.Map.mem id1 terms then warn_bound_again id1 in (names, terms) | _ -> subst @@ -250,12 +250,11 @@ let matches_core convert allow_partial_app allow_bound_rels pat c = | _ -> raise PatternMatchingFailure in - let names, terms = sorec [] (Id.Map.empty, []) pat c in - (names, List.sort (fun (a, _) (b, _) -> Id.compare a b) terms) + sorec [] (Id.Map.empty, Id.Map.empty) pat c let matches_core_closed convert allow_partial_app pat c = let names, subst = matches_core convert allow_partial_app false pat c in - (names, List.map (fun (a,(_,b)) -> (a,b)) subst) + (names, Id.Map.map snd subst) let extended_matches = matches_core None true true @@ -286,7 +285,7 @@ let matches_head pat c = let authorized_occ partial_app closed pat c mk_ctx next = try let sigma = matches_core_closed None partial_app pat c in - if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) + if closed && Id.Map.exists (fun _ c -> not (closed0 c)) (snd sigma) then Lazy.force next else mkresult sigma (mk_ctx (mkMeta special_meta)) next with PatternMatchingFailure -> Lazy.force next diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 5e4e5eb97..d695e8a45 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -203,7 +203,7 @@ let instantiate_pattern sigma lvar c = let rec aux vars = function | PVar id as x -> (try - let ctx,c = List.assoc id lvar in + let ctx,c = Id.Map.find id lvar in try let inst = List.map (fun id -> mkRel (List.index (Name id) vars)) ctx in @@ -213,7 +213,7 @@ let instantiate_pattern sigma lvar c = let vars = List.map_filter (function Name id -> Some id | _ -> None) vars in error_instantiate_pattern id (List.subtract ctx vars) - with Not_found (* List.assoc failed *) -> + with Not_found (* Map.find failed *) -> x) | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.") | c -> diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 4a4649cca..5cc4049ba 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -53,7 +53,7 @@ val pattern_of_glob_constr : glob_constr -> patvar list * constr_pattern val instantiate_pattern : - Evd.evar_map -> (Id.t * (Id.t list * constr)) list -> + Evd.evar_map -> extended_patvar_map -> constr_pattern -> constr_pattern val lift_pattern : int -> constr_pattern -> constr_pattern diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 31cf52eac..a8cdfd869 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -897,7 +897,7 @@ let contextually byhead (occs,c) f env sigma t = else not (List.mem !pos locs) in incr pos; if ok then - let subst' = List.map (on_snd (traverse envc)) subst in + let subst' = Id.Map.map (traverse envc) subst in f subst' env sigma t else if byhead then (* find other occurrences of c in t; TODO: ensure left-to-right *) |