diff options
Diffstat (limited to 'proofs/pfedit.ml')
| -rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 90f20a738..cab86721f 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -69,9 +69,6 @@ let cook_proof hook = | (i,([e],cg,str,h)) -> (i,(e,cg,str,h)) | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.") -let xml_cook_proof = ref (fun _ -> ()) -let set_xml_cook_proof f = xml_cook_proof := f - let get_pftreestate () = Proof_global.give_me_the_proof () |