diff options
| author | Amin Timany | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /tactics | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 8 | ||||
| -rw-r--r-- | tactics/hints.ml | 3 |
3 files changed, 12 insertions, 3 deletions
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 8d8e198119..99761437eb 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -47,7 +47,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = (nf c', Evd.evar_universe_context sigma), eff else let mib,mip = Inductive.lookup_mind_specif env ind in - let ctx = Declareops.inductive_context mib in + let ctx = Declareops.inductive_polymorphic_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in let ectx = Evd.evar_universe_context_of ctxset in @@ -60,7 +60,7 @@ let build_induction_scheme_in_type dep sort ind = let sigma = Evd.from_env env in let ctx = let mib,mip = Inductive.lookup_mind_specif env ind in - Declareops.inductive_context mib + Declareops.inductive_polymorphic_context mib in let u = Univ.UContext.instance ctx in let ctxset = Univ.ContextSet.of_context ctx in diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 77f927f2df..da432beadc 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -10,6 +10,14 @@ open Ind_tables (** Induction/recursion schemes *) +val optimize_non_type_induction_scheme : + 'a Ind_tables.scheme_kind -> + Indrec.dep_flag -> + Term.sorts_family -> + 'b -> + Names.inductive -> + (Constr.constr * Evd.evar_universe_context) * Safe_typing.private_constants + val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind diff --git a/tactics/hints.ml b/tactics/hints.ml index 681db5d08e..2fc8baa895 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1306,7 +1306,8 @@ let interp_hints poly = List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in - empty_hint_info, mib.Declarations.mind_polymorphic, true, + empty_hint_info, + (Declareops.inductive_is_polymorphic mib), true, PathHints [gr], IsGlobRef gr) in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) | HintsExtern (pri, patcom, tacexp) -> |