From 56ff0c9c1475fdfe74af760e4e9fff96738c2c64 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 14 Apr 2018 11:12:00 +0200 Subject: Cleaning, documentation, uniformisation of the Coq extension of List. Still some discrepancies though. E.g.: - some functions taking an equality as arguments have suffix `_f` but not all; - the functions possibly raising an error have still different kinds of failure (Failure, Invalid_argument, Not_found or IndexOutOfRange, and when in the first two cases, with no unique rules in the style of the associated string - we thus avoid to document the exact string used). There are a few semantics changes: - skipn_at_least now raises a `Failure` if its argument is negative; - map3 raises an Invalid_argument "List.map3" rather than Invalid_argument "map3" and similarly for map4 - internally, map3 and map4 are now tail-recursive (by uniformity); - internally, split3 and combine3 are now tail-recursive (by uniformity); - filter is now "smart" by default and smartfilter is deprecated; - smartmap is now tail-recursive by default. --- tactics/hints.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tactics') diff --git a/tactics/hints.ml b/tactics/hints.ml index a86103d57..d3acb5aa5 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -672,7 +672,7 @@ struct let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l - let remove_sdl p sdl = List.Smart.filter p sdl + let remove_sdl p sdl = List.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -684,7 +684,7 @@ struct let filter (_, h) = match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db -- cgit v1.2.3