diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 3e41439c8..76f1d8dd7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -721,9 +721,7 @@ open Decl_kinds | Opaque (Some l) -> keyword "Qed" ++ spc() ++ str"export" ++ prlist_with_sep (fun () -> str", ") pr_lident l) - | Some (id,th) -> (match th with - | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id - | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id) + | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id ) | VernacExactProof c -> return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) |