diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 16:17:09 +0000 |
| commit | f8394a52346bf1e6f98e7161e75fb65bd0631391 (patch) | |
| tree | ae133cc5207283e8c5a89bb860435b37cbf6ecdb /tactics/eauto.ml4 | |
| parent | 6dae53d279afe2b8dcfc43dd2aded9431944c5c8 (diff) | |
Moving Utils.list_* to a proper CList module, which includes stdlib
List module. That way, an "open Util" in the header permits using
any function of CList in the List namespace (and in particular, this
permits optimized reimplementations of the List functions, as, for
example, tail-rec implementations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15801 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/eauto.ml4')
| -rw-r--r-- | tactics/eauto.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 28840669f..fd5fbe25a 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -119,11 +119,11 @@ and e_my_find_search db_list local_db hdc concl = let hdc = head_of_constr_reference hdc in let hintl = if occur_existential concl then - list_map_append (fun db -> + List.map_append (fun db -> let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list) else - list_map_append (fun db -> + List.map_append (fun db -> let flags = {auto_unif_flags with modulo_delta = Hint_db.transparent_state db} in List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list) in @@ -261,7 +261,7 @@ module SearchProblem = struct { depth = pred s.depth; tacres = res; dblist = s.dblist; last_tactic = pp; prev = ps; localdb = - list_addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) + List.addn (nbgl'-nbgl) (List.hd s.localdb) s.localdb }) l in List.sort compare (assumption_tacs @ intro_tac @ rec_tacs) @@ -364,7 +364,7 @@ let eauto ?(debug=Off) np lems dbnames = let full_eauto ?(debug=Off) n lems gl = let dbnames = current_db_names () in - let dbnames = list_remove "v62" dbnames in + let dbnames = List.remove "v62" dbnames in let db_list = List.map searchtable_map dbnames in tclTRY (e_search_auto debug n lems db_list) gl |