From e4c43d45c6fe5267ad72a1be64d6328470f2a18e Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 5 Jul 2018 17:02:03 +0100
Subject: Coq: missing existential building for ranges

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

(limited to 'src')

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