diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 27 | ||||
| -rw-r--r-- | toplevel/search.ml | 7 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 3 |
3 files changed, 25 insertions, 12 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 55475a378..e17038a4f 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -69,23 +69,34 @@ let abstract_inductive hyps nparams inds = in (params',ind'') let refresh_polymorphic_type_of_inductive (_,mip) = - mip.mind_arity.mind_user_arity + match mip.mind_arity with + | RegularArity s -> s.mind_user_arity, Univ.ContextSet.empty + | TemplateArity ar -> + let ctx = List.rev mip.mind_arity_ctxt in + let univ, uctx = Universes.new_global_univ () in + mkArity (List.rev ctx, Type univ), uctx let process_inductive (sechyps,abs_ctx) modlist mib = let nparams = mib.mind_nparams in + let univctx = ref Univ.ContextSet.empty in let inds = Array.map_to_list (fun mip -> - let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in - let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in - (mip.mind_typename, - arity, - Array.to_list mip.mind_consnames, - Array.to_list lc)) + let ty, uctx = refresh_polymorphic_type_of_inductive (mib,mip) in + let () = univctx := Univ.ContextSet.union uctx !univctx in + let arity = expmod_constr modlist ty in + let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in + (mip.mind_typename, + arity, + Array.to_list mip.mind_consnames, + Array.to_list lc)) mib.mind_packets in let sechyps' = map_named_context (expmod_constr modlist) sechyps in let (params',inds') = abstract_inductive sechyps' nparams inds in - let univs = Univ.UContext.union abs_ctx mib.mind_universes in + let univs = Univ.UContext.union abs_ctx + (Univ.UContext.union (Univ.ContextSet.to_context !univctx) + mib.mind_universes) + in { mind_entry_record = mib.mind_record <> None; mind_entry_finite = mib.mind_finite; mind_entry_params = params'; diff --git a/toplevel/search.ml b/toplevel/search.ml index 1535ae617..37403504d 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -60,14 +60,15 @@ let iter_declarations (fn : global_reference -> env -> constr -> unit) = with Not_found -> (* we are in a section *) () end | "CONSTANT" -> let cst = Global.constant_of_delta_kn kn in - let typ, _ = Environ.constant_type_in_ctx env cst in - fn (ConstRef cst) env typ + let gr = ConstRef cst in + let typ = Global.type_of_global_unsafe gr in + fn gr env typ | "INDUCTIVE" -> let mind = Global.mind_of_delta_kn kn in let mib = Global.lookup_mind mind in let iter_packet i mip = let ind = (mind, i) in - let i = (ind, Univ.UContext.instance mib.mind_universes) in + let i = (ind, Inductive.inductive_instance mib) in let typ = Inductiveops.type_of_inductive env i in let () = fn (IndRef ind) env typ in let len = Array.length mip.mind_user_lc in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 02e59a227..67ca1b666 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -252,7 +252,8 @@ let print_namespace ns = print_list pr_id qn in let print_constant k body = - let t = body.Declarations.const_type in + (* FIXME: universes *) + let t = Typeops.type_of_constant_type (Global.env ()) body.Declarations.const_type in print_kn k ++ str":" ++ spc() ++ Printer.pr_type t in let matches mp = match match_modulepath ns mp with |