diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4e2193c1..90276cb3 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1929,6 +1929,7 @@ let doc_val pat exp = in let env = env_of exp in let typ = expand_range_type (Env.expand_synonyms env (typ_of exp)) in + let ctxt = { empty_ctxt with debug = List.mem (string_of_id id) (!opt_debug_on) } in let id, opt_unpack = match destruct_exist env typ with | None -> id, None @@ -1943,7 +1944,7 @@ let doc_val pat exp = let idpp = doc_id id in let basepp = group (string "Definition" ^^ space ^^ idpp ^^ typpp ^^ space ^^ coloneq ^/^ - doc_exp_lem empty_ctxt false exp ^^ dot) ^^ hardline + doc_exp_lem ctxt false exp ^^ dot) ^^ hardline in match opt_unpack with | None -> basepp ^^ hardline |