match grafite_status.GrafiteTypes.proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
match grafite_status.GrafiteTypes.proof_status with
GrafiteTypes.Incomplete_proof
{GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;