diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index b12378c56..4dd00301f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -38,7 +38,7 @@ let abstract_inductive hyps nparams inds = let ntyp = List.length inds in let nhyp = named_context_length hyps in let args = instance_from_named_context (List.rev hyps) in - let subs = List.tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in + let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in let inds' = List.map (function (tname,arity,cnames,lc) -> |