From 5145c143cfd69617ac72932c4cf44c0d9de9d6df Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 24 May 2018 13:41:16 +0100
Subject: Coq: record conditionals in the context for constraint solving

---
 src/pretty_print_coq.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index efdb770d..4da256a6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -957,7 +957,7 @@ let doc_exp_lem, doc_let_lem =
       | _ -> prefix 2 1 (string "else") (top_exp ctxt false e)
     in
     (prefix 2 1
-      (soft_surround 2 1 if_pp (top_exp ctxt true c) (string "then"))
+      (soft_surround 2 1 if_pp (string "sumbool_of_bool" ^^ space ^^ parens (top_exp ctxt true c)) (string "then"))
       (top_exp ctxt false t)) ^^
     break 1 ^^
     else_pp
@@ -1452,7 +1452,7 @@ string "Require Import String."; hardline;
        [string "(*" ^^ (string top_line) ^^ string "*)";hardline;
         (separate_map hardline)
           (fun lib -> separate space [string "Require Import";string lib] ^^ dot) defs_modules;hardline;
-string "Require Import List. Import ListNotations.";
+string "Require Import List. Import ListNotations. Require Import Sumbool.";
         hardline;
         separate empty (List.map doc_def defs);
         hardline]);
-- 
cgit v1.2.3