From 0a51137f7ff80afdcf216d85cd8be25a531bc39b Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 15 Jun 2014 13:24:41 +0200 Subject: - Fix xml plugin treatment of inductives. - Move HoTT bug #30 to closed --- plugins/xml/xmlcommand.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'plugins/xml') diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml index 8f47859da..ef5e18201 100644 --- a/plugins/xml/xmlcommand.ml +++ b/plugins/xml/xmlcommand.ml @@ -244,15 +244,16 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite = let {Declarations.mind_consnames=consnames ; Declarations.mind_typename=typename } = p in - let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),Univ.Instance.empty)(*FIXME*) in - let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),Univ.Instance.empty)(*FIXME*) in - let cons = + let inst = Univ.UContext.instance mib.Declarations.mind_universes in + let arity = Inductive.type_of_inductive (Global.env()) ((mib,p),inst) in + let lc = Inductiveops.arities_of_constructors (Global.env ()) ((sp,!tyno),inst) in + let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) - (Array.mapi - (fun j x ->(x,Unshare.unshare lc.(j))) consnames) - [] + (Array.mapi + (fun j x ->(x,Unshare.unshare lc.(j))) consnames) + [] ) - in + in (typename,finite,Unshare.unshare arity,cons)::i ) packs [] in -- cgit v1.2.3