diff options
| author | Emilio Jesus Gallego Arias | 2019-02-19 18:07:19 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-19 18:07:19 +0100 |
| commit | c3cc72ccf586703ed009a8bdd5df8d40b0384ab2 (patch) | |
| tree | 06a68b153c71a5cd8caf57572ffb59e52f507265 /plugins | |
| parent | 6e3850ce5092d5cb432ef917ae6ee79225089f6a (diff) | |
| parent | a8a26c87d52c30e5e5d1ba76f1920e8bc68bcd45 (diff) | |
Merge PR #9297: Two fixes in printing notations with patterns
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
Diffstat (limited to 'plugins')
| -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) |