aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/instances.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/instances.ml')
-rw-r--r--plugins/firstorder/instances.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index baf1972e6..12b2304ac 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -112,7 +112,7 @@ let mk_open_instance id gl m t=
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
- let revt=substl (List.tabulate (fun i->mkRel (m-i)) m) t in
+ let revt=substl (List.init m (fun i->mkRel (m-i))) t in
let rec aux n avoid=
if n=0 then [] else
let nid=(fresh_id avoid var_id gl) in