aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index a0f565ce36..1b2ba0e87a 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -179,7 +179,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.init n (fun i -> Id.of_string("x"^string_of_int i)) in
let res = ref [||] in
let get_res ist =
let l = List.map (fun id -> List.assoc id ist.lfun) lid in