diff options
| author | Brian Campbell | 2018-05-24 13:41:16 +0100 |
|---|---|---|
| committer | Brian Campbell | 2018-05-24 16:10:48 +0100 |
| commit | 5145c143cfd69617ac72932c4cf44c0d9de9d6df (patch) | |
| tree | c8664bd4fd5035d31e8f53e09dec1cdb2fc291c1 | |
| parent | 52965bdc2875ea35f5433e22307a1e951d054417 (diff) | |
Coq: record conditionals in the context for constraint solving
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files 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]); |