diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-04 13:38:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:11:13 +0200 |
| commit | 4457e6d75affd20c1c13c0d798c490129525bcb5 (patch) | |
| tree | b5eeffe5f1a07c439fe704a6d60b2b036110df7f /tactics | |
| parent | a960c4db9ae93a6445f9db620f96f62b397ba8b5 (diff) | |
More precise type for universe entries.
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/ind_tables.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.ml | 8 |
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 |