diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 10:44:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-04 10:44:42 +0200 |
| commit | 01128a2ff774f0ef249ee54a67e88d49ae254a4d (patch) | |
| tree | 5b1dc69b34988ad1c60f8cadcb9233749c917876 /tactics | |
| parent | c2ceb06d88c63814dd704cd505420dc44841c026 (diff) | |
| parent | 1d7fef8272d13a6e57bc46218d4a89c7e725c4d2 (diff) | |
Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension of List
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hints.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hints.ml b/tactics/hints.ml index 636edeb34..4b77418ff 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 |