diff options
| author | Hugo Herbelin | 2018-12-27 12:44:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-02-19 15:06:00 +0100 |
| commit | a8a26c87d52c30e5e5d1ba76f1920e8bc68bcd45 (patch) | |
| tree | af00b4d6fa94aa1535829d3772567916024c9a4d /plugins/funind | |
| parent | 21bcc5f6fc8db1ccad16dea89f1705a799c1d090 (diff) | |
Notations: Fixing a printing bug with patterns.
Parameters had to be removed in cases_pattern_of_glob_constr.
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) |