aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-28 18:23:36 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-07-28 18:23:36 +0200
commit3828267b6dcd60088a11fe0b9613871e4fc7c54f (patch)
treeacba2a7cbfb775ce570a13f1894a6f6161d3f617 /tactics
parenteaff3b36a178416f1828d75a4d46afc687953cea (diff)
parent906b48ff401f22be6059a6cdde8723b858102690 (diff)
Merge PR #888: Stronger kernel types
Diffstat (limited to 'tactics')
-rw-r--r--tactics/ind_tables.ml8
-rw-r--r--tactics/tactics.ml8
2 files changed, 11 insertions, 5 deletions
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 0407c1e36..7f087ea01 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,14 +123,18 @@ let define internal id c p univs =
let ctx = Evd.normalize_evar_universe_context univs in
let c = Vars.subst_univs_fn_constr
(Universes.make_opt_subst (Evd.evar_universe_context_subst ctx)) c in
+ let univs = Evd.evar_context_universe_context ctx in
+ let univs =
+ if p then Polymorphic_const_entry univs
+ else Monomorphic_const_entry univs
+ in
let entry = {
const_entry_body =
Future.from_val ((c,Univ.ContextSet.empty),
Safe_typing.empty_private_constants);
const_entry_secctx = None;
const_entry_type = None;
- const_entry_polymorphic = p;
- const_entry_universes = Evd.evar_context_universe_context ctx;
+ const_entry_universes = univs;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8a95ad177..cb905e749 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5004,8 +5004,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
in
let cst = Impargs.with_implicit_protection cst () in
let lem =
- if const.Entries.const_entry_polymorphic then
- let uctx = Univ.ContextSet.of_context const.Entries.const_entry_universes in
+ match const.Entries.const_entry_universes with
+ | Entries.Polymorphic_const_entry uctx ->
+ let uctx = Univ.ContextSet.of_context uctx in
(** Hack: the kernel may generate definitions whose universe variables are
not the same as requested in the entry because of constraints delayed
in the body, even in polymorphic mode. We mimick what it does for now
@@ -5014,7 +5015,8 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK =
let uctx = Univ.ContextSet.to_context (Univ.ContextSet.union uctx body_uctx) in
let u = Univ.UContext.instance uctx in
mkConstU (cst, EInstance.make u)
- else mkConst cst
+ | Entries.Monomorphic_const_entry _ ->
+ mkConst cst
in
let evd = Evd.set_universe_context evd ectx in
let open Safe_typing in