diff options
| author | Matthieu Sozeau | 2015-11-20 20:18:11 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-20 20:19:16 +0100 |
| commit | 8d93301045c45ec48c85ecae2dfb3609e5e4695f (patch) | |
| tree | f0d9fdf1d8562d3ee5d1a3fdb82c96dd4acdca09 | |
| parent | 2b47c0d1b492424c39477f9d4ec262e4d093be92 (diff) | |
Univs: generation of induction schemes should not generated useless
instances for each of the inductive in the same block but reuse the
original universe context shared by all of them. Also do not force
schemes to become universe polymorphic.
| -rw-r--r-- | toplevel/indschemes.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index f16e6e3f3f..00197bd668 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -128,7 +128,7 @@ let define id internal ctx c t = { const_entry_body = c; const_entry_secctx = None; const_entry_type = t; - const_entry_polymorphic = true; + const_entry_polymorphic = Flags.is_universe_polymorphism (); const_entry_universes = snd (Evd.universe_context ctx); const_entry_opaque = false; const_entry_inline_code = false; @@ -360,12 +360,21 @@ requested let do_mutual_induction_scheme lnamedepindsort = let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort and env0 = Global.env() in - let sigma, lrecspec = + let sigma, lrecspec, _ = List.fold_right - (fun (_,dep,ind,sort) (evd, l) -> - let evd, indu = Evd.fresh_inductive_instance env0 evd ind in - (evd, (indu,dep,interp_elimination_sort sort) :: l)) - lnamedepindsort (Evd.from_env env0,[]) + (fun (_,dep,ind,sort) (evd, l, inst) -> + let evd, indu, inst = + match inst with + | None -> + let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in + let ctxs = Univ.ContextSet.of_context ctx in + let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in + let u = Univ.UContext.instance ctx in + evd, (ind,u), Some u + | Some ui -> evd, (ind, ui), inst + in + (evd, (indu,dep,interp_elimination_sort sort) :: l, inst)) + lnamedepindsort (Evd.from_env env0,[],None) in let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = |