+let (get_proof, set_proof, has_proof) =
+ let (current_proof: MatitaTypes.proof option ref) = ref None in
+ ((fun () ->
+ match !current_proof with
+ | Some proof -> proof
+ | None -> assert false),
+ (fun proof -> current_proof := Some proof),
+ (fun () -> !current_proof <> None))