From 98012682e6f1b3d9a786d71bc4567002a454ec7a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 13 Sep 2018 18:01:52 +0100
Subject: Coq: remove an obsolete specialisation Broke E_internal_plet on some
 simple existential types

---
 src/pretty_print_coq.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'src')

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index 00547db1..a61562e1 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -1505,11 +1505,6 @@ let doc_exp, doc_let =
                     when not (is_enum (env_of e1) id) ->
                       let full_typ = (expand_range_type typ) in
                       let binder = match destruct_exist (env_of e1) full_typ with
-                        | Some ([kid], NC_aux (NC_true,_),
-                                Typ_aux (Typ_app (Id_aux (Id "atom",_),
-                                                  [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
-                            when Kid.compare kid kid' == 0 ->
-                           parens (separate space [doc_id id; colon; string "Z"])
                         | Some ([kid], nc,
                                 Typ_aux (Typ_app (Id_aux (Id "atom",_),
                                                   [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid',_)),_)]),_))
-- 
cgit v1.2.3