Module Proof_global
type t= Declare.Proof.t
val map_proof : (Proof.t -> Proof.t) -> Declare.Proof.t -> Declare.Proof.tval get_proof : Declare.Proof.t -> Proof.t
type opacity_flag= Declare.opacity_flag=|Opaque|Transparent
Proof_globaltype t = Declare.Proof.tval map_proof : (Proof.t -> Proof.t) -> Declare.Proof.t -> Declare.Proof.tval get_proof : Declare.Proof.t -> Proof.ttype opacity_flag = Declare.opacity_flag = | Opaque |
| Transparent |