diff options
author | 2008-02-22 13:39:13 +0000 | |
---|---|---|
committer | 2008-02-22 13:39:13 +0000 | |
commit | e8ef565dadd110329f806fa3c281055fcd807440 (patch) | |
tree | e0f069cb228ee77524800d98c53291014c1a1315 /proofs/pfedit.ml | |
parent | 2e67ff1b33d05b9efc020de664f3200f9ff0d479 (diff) |
Merge with lmamane's private branch:
- New vernac command "Delete"
- New vernac command "Undo To"
- Added a few hooks used by new contrib/interface
- Beta/incomplete version of dependency generation and dumping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10580 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/pfedit.ml')
-rw-r--r-- | proofs/pfedit.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c6cb86dc9..81216d169 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -204,13 +204,14 @@ let current_proof_depth() = let xml_cook_proof = ref (fun _ -> ()) let set_xml_cook_proof f = xml_cook_proof := f -let cook_proof () = +let cook_proof k = let (pfs,ts) = get_state() and ident = get_current_proof_name () in let {evar_concl=concl} = ts.top_goal and strength = ts.top_strength in let pfterm = extract_pftreestate pfs in !xml_cook_proof (strength,pfs); + k pfs; (ident, ({ const_entry_body = pfterm; const_entry_type = Some concl; |