diff options
Diffstat (limited to 'vernac/ppvernac.ml')
| -rw-r--r-- | vernac/ppvernac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index baaf8aa849..7a2e6d8b03 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -791,7 +791,7 @@ let string_of_definition_object_kind = let open Decls in function return (keyword "Admitted") | VernacEndProof (Proved (opac,o)) -> return ( - let open Proof_global in + let open Declare in match o with | None -> (match opac with | Transparent -> keyword "Defined" |