diff options
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 871a7f15..2235be4a 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -395,7 +395,7 @@ let mk_constant_obj id bo ty variables hyps = ty,params) ;; -let mk_inductive_obj sp packs variables nparams hyps finite = +let mk_inductive_obj sp mib packs variables nparams hyps finite = let module D = Declarations in let hyps = string_list_of_named_context_list hyps in let params = filter_params variables hyps in @@ -406,9 +406,9 @@ let mk_inductive_obj sp packs variables nparams hyps finite = (fun p i -> decr tyno ; let {D.mind_consnames=consnames ; - D.mind_typename=typename ; - D.mind_nf_arity=arity} = p + D.mind_typename=typename } = p in + let arity = Inductive.type_of_inductive (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) @@ -524,11 +524,12 @@ let print internal glob_ref kind xml_library_root = G.lookup_constant kn in Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps | Ln.IndRef (kn,_) -> + let mib = G.lookup_mind kn in let {D.mind_nparams=nparams; D.mind_packets=packs ; D.mind_hyps=hyps; - D.mind_finite=finite} = G.lookup_mind kn in - Cic2acic.Inductive kn,mk_inductive_obj kn packs variables nparams hyps finite + 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") in |