From f8394a52346bf1e6f98e7161e75fb65bd0631391 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 14 Sep 2012 16:17:09 +0000 Subject: 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 --- plugins/setoid_ring/newring.ml4 | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index f540349ed8..f838b56c6e 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -87,7 +87,7 @@ let interp_map l c = with Not_found -> None let interp_map l t = - try Some(list_assoc_f eq_constr t l) with Not_found -> None + try Some(List.assoc_f eq_constr t l) with Not_found -> None let protect_maps = ref Stringmap.empty let add_map s m = protect_maps := Stringmap.add s m !protect_maps @@ -194,7 +194,7 @@ let dummy_goal env = Evd.sigma = sigma} let exec_tactic env n f args = - let lid = list_tabulate(fun i -> id_of_string("x"^string_of_int i)) n in + let lid = List.tabulate(fun i -> id_of_string("x"^string_of_int i)) n in let res = ref [||] in let get_res ist = let l = List.map (fun id -> List.assoc id ist.lfun) lid in @@ -834,7 +834,7 @@ let ring_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND ring_lookup | [ "ring_lookup" tactic0(f) "[" constr_list(lH) "]" ne_constr_list(lrt) ] -> - [ let (t,lr) = list_sep_last lrt in ring_lookup f lH lr t] + [ let (t,lr) = List.sep_last lrt in ring_lookup f lH lr t] END @@ -1162,5 +1162,5 @@ let field_lookup (f:glob_tactic_expr) lH rl t gl = TACTIC EXTEND field_lookup | [ "field_lookup" tactic(f) "[" constr_list(lH) "]" ne_constr_list(lt) ] -> - [ let (t,l) = list_sep_last lt in field_lookup f lH l t ] + [ let (t,l) = List.sep_last lt in field_lookup f lH l t ] END -- cgit v1.2.3