From 4932765be036afe3433e13c3473f602f35034f4c Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 24 May 2018 16:04:21 +0100
Subject: Coq: need None special case here, too

---
 src/pretty_print_coq.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3