diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4da256a6..f156b321 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -503,6 +503,8 @@ let is_ctor env id = match Env.lookup_id id env with be removed prior to pp. The latter two have never yet been seen *) let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot))) = match p with + (* Special case translation of the None constructor to remove the unit arg *) + | P_app(id, _) when string_of_id id = "None" -> string "None" | P_app(id, ((_ :: _) as pats)) -> let ppp = doc_unop (doc_id_ctor id) (parens (separate_map comma (doc_pat ctxt true) pats)) in |