diff options
| author | Brian Campbell | 2018-09-13 18:01:52 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-09-17 17:03:00 +0100 |
| commit | 98012682e6f1b3d9a786d71bc4567002a454ec7a (patch) | |
| tree | ddfa57c5e0b28633af06718d0907c8fe9525e03e /src | |
| parent | c6a03fe03e9e19978cceb64562acfffd7ca066ea (diff) | |
Coq: remove an obsolete specialisation
Broke E_internal_plet on some simple existential types
Diffstat (limited to 'src')
| -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',_)),_)]),_)) |