diff options
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 6df8c5df..5f4d349c 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -946,6 +946,9 @@ let doc_exp_lem, doc_let_lem = (* TODO: more sophisticated check *) match destruct_exist env arg_ty, destruct_exist env typ_from_fn with | Some _, None -> parens (string "projT1 " ^^ arg_pp) + (* Usually existentials have already been built elsewhere, but this + is useful for (e.g.) ranges *) + | None, Some _ -> parens (string "build_ex " ^^ arg_pp) | _, _ -> arg_pp in let epp = hang 2 (flow (break 1) (call :: List.map2 doc_arg args arg_typs)) in |