diff options
| author |  sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-30 15:20:37 +0000 |
|---|---|---|
| committer | sacerdot <sacerdot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-03-30 15:20:37 +0000 |
| commit | 1fd9493d186f82e908412fbc3568f1f2358d8606 (patch) | |
| tree | 16f6e39526ff815a3c4c0eba74cf9c8062941617 | |
| parent | 0293882732f81c18057bc071646c9a2cd77ed357 (diff) | |
declare_internal_constant behaved as declare_constant for proofs (e.g.
*_subproof)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5617 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index ace8a7435..628277b1a 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -533,7 +533,7 @@ let print internal glob_ref xml_library_root = (* show dest *) (* where dest is either None (for stdout) or (Some filename) *) (* pretty prints via Xml.pp the proof in progress on dest *) -let show_pftreestate fn (kind,pftst) id = +let show_pftreestate internal fn (kind,pftst) id = let str = Names.string_of_id id in let pf = Tacmach.proof_of_pftreestate pftst in let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in @@ -545,7 +545,7 @@ let show_pftreestate fn (kind,pftst) id = let env = Global.env () in let obj = mk_current_proof_obj id val0 typ evar_map env in let uri = Cic2acic.uri_of_declaration id Cic2acic.Constant in - print_object_kind uri (kind_of_goal kind); + if not internal then print_object_kind uri (kind_of_goal kind); print_object uri obj evar_map (Some (Tacmach.evc_of_pftreestate pftst,unshared_pf,proof_tree_to_constr, proof_tree_to_flattened_proof_tree)) fn @@ -554,7 +554,7 @@ let show_pftreestate fn (kind,pftst) id = let show fn = let pftst = Pfedit.get_pftreestate () in let (id,kind,_,_) = Pfedit.current_proof_statement () in - show_pftreestate fn (kind,pftst) id + show_pftreestate false fn (kind,pftst) id ;; @@ -589,7 +589,7 @@ let _ = (* It is a proof. Let's export it starting from the proof-tree *) (* I saved in the Pfedit.set_xml_cook_proof callback. *) let fn = filename_of_path xml_library_root kn Cic2acic.Constant in - show_pftreestate fn pftreestate + show_pftreestate internal fn pftreestate (Names.id_of_label (Names.label kn)) ; proof_to_export := None) ;; |