diff options
Diffstat (limited to 'plugins/xml/xmlcommand.ml')
| -rw-r--r-- | plugins/xml/xmlcommand.ml | 46 |
1 files changed, 9 insertions, 37 deletions
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 7e7f890f..1037bbf0 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * The HELM Project / The EU MoWGLI Project *) (* * University of Bologna *) @@ -527,8 +527,10 @@ let print internal glob_ref kind xml_library_root = Cic2acic.Variable kn,mk_variable_obj id body typ | Ln.ConstRef kn -> let id = N.id_of_label (N.con_label kn) in - let {D.const_body=val0 ; D.const_type = typ ; D.const_hyps = hyps} = - G.lookup_constant kn in + let cb = G.lookup_constant kn in + let val0 = D.body_of_constant cb in + let typ = cb.D.const_type in + let hyps = cb.D.const_hyps in let typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> @@ -557,43 +559,13 @@ let print_ref qid fn = (* where dest is either None (for stdout) or (Some filename) *) (* pretty prints via Xml.pp the proof in progress on dest *) let show_pftreestate internal fn (kind,pftst) id = - let pf = Tacmach.proof_of_pftreestate pftst in - let typ = (Proof_trees.goal_of_proof pf).Evd.evar_concl in - let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, - unshared_pf - = - Proof2aproof.extract_open_pftreestate pftst in - let env = Global.env () in - let obj = - mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in - let uri = - match kind with - Decl_kinds.Local, _ -> - let uri = - "cic:/" ^ String.concat "/" - (Cic2acic.token_list_of_path (Lib.cwd ()) id Cic2acic.TVariable) - in - let kind_of_var = "VARIABLE","LocalFact" in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri kind_of_var - ); uri - | Decl_kinds.Global, _ -> - let uri = Cic2acic.uri_of_declaration id Cic2acic.TConstant in - (match internal with - | Declare.KernelSilent -> () - | _ -> print_object_kind uri (kind_of_global_goal kind) - ); uri - in - 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 -;; + if true then + Util.anomaly "Xmlcommand.show_pftreestate is not supported in this version." let show fn = let pftst = Pfedit.get_pftreestate () in let (id,kind,_,_) = Pfedit.current_proof_statement () in - show_pftreestate Declare.KernelVerbose fn (kind,pftst) id + show_pftreestate false fn (kind,pftst) id ;; @@ -680,7 +652,7 @@ let _ = end ; Option.iter (fun fn -> - let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in + let coqdoc = Filename.concat Envars.coqbin ("coqdoc" ^ Coq_config.exec_extension) in let options = " --html -s --body-only --no-index --latin1 --raw-comments" in let command cmd = if Sys.command cmd <> 0 then |