diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index b6b1c7b6..f286d2c8 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -408,7 +408,7 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let {D.mind_consnames=consnames ; D.mind_typename=typename } = p in - let arity = Inductive.type_of_inductive (mib,p) in + let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) @@ -522,6 +522,7 @@ let print internal glob_ref kind xml_library_root = 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 typ = Typeops.type_of_constant_type (Global.env()) typ in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> let mib = G.lookup_mind kn in @@ -531,7 +532,7 @@ let print internal glob_ref kind xml_library_root = D.mind_finite=finite} = mib in Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite | Ln.ConstructRef _ -> - Util.anomaly ("print: this should not happen") + Util.error ("a single constructor cannot be printed in XML") in let fn = filename_of_path xml_library_root tag in let uri = Cic2acic.uri_of_kernel_name tag in @@ -547,14 +548,12 @@ 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 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 let val0,evar_map,proof_tree_to_constr,proof_tree_to_flattened_proof_tree, unshared_pf = Proof2aproof.extract_open_pftreestate pftst in - let kn = Lib.make_kn id in let env = Global.env () in let obj = mk_current_proof_obj (fst kind = Decl_kinds.Local) id val0 typ evar_map env in |