diff options
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 02964d7ba5..ba0a3bbb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -321,12 +321,10 @@ let build_constructors_of_type ind' argl = construct in let argl = - if List.is_empty argl - then - Array.to_list - (Array.init (cst_narg - npar) (fun _ -> mkGHole ()) - ) - else argl + if List.is_empty argl then + List.make cst_narg (mkGHole ()) + else + List.make npar (mkGHole ()) @ argl in let pat_as_term = mkGApp(mkGRef (ConstructRef(ind',i+1)),argl) |