diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 5 |
1 files changed, 0 insertions, 5 deletions
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',_)),_)]),_)) |