diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-23 22:17:33 +0000 |
| commit | bb5e6d7c39211349d460db0b61b2caf3d099d5b6 (patch) | |
| tree | e14b120edc5fedcb1a0a114218d1cdaa0f887ed4 /pretyping | |
| parent | 4e20ed9e5c1608226f0d736df10bb82fc402e7a2 (diff) | |
cList: a few alternative to hashtbl-based uniquize, distinct, subset
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16924 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarsolve.ml | 11 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
3 files changed, 9 insertions, 6 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index fc5fc0d2c..aa8f2d08e 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -781,17 +781,20 @@ let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' = * such that "hyps' |- ?e : T" *) +let set_of_evctx l = + List.fold_left (fun s (id,_,_) -> Id.Set.add id s) Id.Set.empty l + let filter_candidates evd evk filter candidates = let evi = Evd.find_undefined evd evk in let candidates = match candidates with | None -> evi.evar_candidates - | Some _ -> candidates in + | Some _ -> candidates + in match candidates,filter with | None,_ | _, None -> candidates | Some l, Some filter -> - let ids = List.map pi1 (List.filter_with filter (evar_context evi)) in - Some (List.filter (fun a -> - List.subset (Id.Set.elements (collect_vars a)) ids) l) + let ids = set_of_evctx (List.filter_with filter (evar_context evi)) in + Some (List.filter (fun a -> Id.Set.subset (collect_vars a) ids) l) let eq_filter f1 f2 = let eq_bool b1 b2 = if b1 then b2 else not b2 in diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 1db40e8db..13eb91393 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -180,7 +180,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = raise Elimconst) args in let reversible_rels = List.map fst li in - if not (List.distinct reversible_rels) then + if not (List.distinct_f Int.compare reversible_rels) then raise Elimconst; List.iteri (fun i t_i -> if not (List.mem_assoc (i+1) li) then diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 2e2389f09..899def8c8 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -696,7 +696,7 @@ let replace_term = replace_term_gen eq_constr except the ones in l *) let error_invalid_occurrence l = - let l = List.uniquize (List.sort Pervasives.compare l) in + let l = List.sort_uniquize Int.compare l in errorlabstrm "" (str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ") ++ prlist_with_sep spc int l ++ str ".") |