aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli11
-rw-r--r--checker/cic.mli4
-rw-r--r--checker/mod_checking.ml2
-rw-r--r--checker/values.ml6
-rw-r--r--interp/declare.ml6
-rw-r--r--kernel/declarations.ml6
-rw-r--r--kernel/declareops.ml4
-rw-r--r--kernel/entries.ml10
-rw-r--r--kernel/indtypes.ml9
-rw-r--r--kernel/mod_typing.ml26
-rw-r--r--kernel/safe_typing.ml12
-rw-r--r--kernel/term_typing.ml46
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--kernel/univ.ml1
-rw-r--r--kernel/univ.mli5
-rw-r--r--kernel/vconv.ml2
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--printing/prettyp.ml14
-rw-r--r--printing/printer.ml4
-rw-r--r--printing/printer.mli1
-rw-r--r--proofs/proof_global.ml12
-rw-r--r--tactics/ind_tables.ml5
-rw-r--r--test-suite/output/UnivBinders.out2
-rw-r--r--vernac/classes.ml34
-rw-r--r--vernac/command.ml15
-rw-r--r--vernac/indschemes.ml6
-rw-r--r--vernac/lemmas.ml19
-rw-r--r--vernac/obligations.ml45
-rw-r--r--vernac/record.ml36
29 files changed, 205 insertions, 146 deletions
diff --git a/API/API.mli b/API/API.mli
index 5c7860671..ad5d5490b 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1417,7 +1417,7 @@ sig
| TemplateArity of 'b
type constant_universes =
- | Monomorphic_const of Univ.UContext.t
+ | Monomorphic_const of Univ.ContextSet.t
| Polymorphic_const of Univ.AUContext.t
type projection_body = {
@@ -1484,7 +1484,7 @@ sig
| MEwith of module_alg_expr * with_declaration
type abstract_inductive_universes =
- | Monomorphic_ind of Univ.UContext.t
+ | Monomorphic_ind of Univ.ContextSet.t
| Polymorphic_ind of Univ.AUContext.t
| Cumulative_ind of Univ.ACumulativityInfo.t
@@ -1551,7 +1551,7 @@ sig
| LocalAssumEntry of constr
type inductive_universes =
- | Monomorphic_ind_entry of Univ.UContext.t
+ | Monomorphic_ind_entry of Univ.ContextSet.t
| Polymorphic_ind_entry of Univ.UContext.t
| Cumulative_ind_entry of Univ.CumulativityInfo.t
@@ -1580,8 +1580,9 @@ sig
type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
- | Monomorphic_const_entry of Univ.UContext.t
+ | Monomorphic_const_entry of Univ.ContextSet.t
| Polymorphic_const_entry of Univ.UContext.t
+ type 'a in_constant_universes_entry = 'a * constant_universes_entry
type 'a definition_entry =
{ const_entry_body : 'a const_entry_body;
(* List of section variables *)
@@ -1592,7 +1593,7 @@ sig
const_entry_universes : constant_universes_entry;
const_entry_opaque : bool;
const_entry_inline_code : bool }
- type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline
+ type parameter_entry = Context.Named.t option * Constr.types in_constant_universes_entry * inline
type projection_entry = {
proj_entry_ind : MutInd.t;
diff --git a/checker/cic.mli b/checker/cic.mli
index 354650964..4a0e706aa 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -208,7 +208,7 @@ type constant_def =
| OpaqueDef of lazy_constr
type constant_universes =
- | Monomorphic_const of Univ.universe_context
+ | Monomorphic_const of Univ.ContextSet.t
| Polymorphic_const of Univ.abstract_universe_context
(** The [typing_flags] are instructions to the type-checker which
@@ -303,7 +303,7 @@ type one_inductive_body = {
}
type abstract_inductive_universes =
- | Monomorphic_ind of Univ.universe_context
+ | Monomorphic_ind of Univ.ContextSet.t
| Polymorphic_ind of Univ.abstract_universe_context
| Cumulative_ind of Univ.abstract_cumulativity_info
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 63e28448f..4357a690e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -29,7 +29,7 @@ let check_constant_declaration env kn cb =
(** [env'] contains De Bruijn universe variables *)
let env' =
match cb.const_universes with
- | Monomorphic_const ctx -> push_context ~strict:true ctx env
+ | Monomorphic_const ctx -> push_context_set ~strict:true ctx env
| Polymorphic_const auctx ->
let ctx = Univ.AUContext.repr auctx in
push_context ~strict:false ctx env
diff --git a/checker/values.ml b/checker/values.ml
index 9e16c8435..5a371164c 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
with a copy we maintain here:
-MD5 f4b00c567a972ae950b9ed10c533fda5 checker/cic.mli
+MD5 56ac4cade33eff3d26ed5cdadb580c7e checker/cic.mli
*)
@@ -215,7 +215,7 @@ let v_projbody =
let v_typing_flags =
v_tuple "typing_flags" [|v_bool; v_bool|]
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context|]; [|v_abs_context|]|]
+let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
let v_cb = v_tuple "constant_body"
[|v_section_ctxt;
@@ -265,7 +265,7 @@ let v_mind_record = Annot ("mind_record",
let v_ind_pack_univs =
v_sum "abstract_inductive_universes" 0
- [|[|v_context|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
+ [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
let v_ind_pack = v_tuple "mutual_inductive_body"
[|Array v_one_ind;
diff --git a/interp/declare.ml b/interp/declare.ml
index dc77981f2..15999f1d1 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -207,7 +207,9 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
let univs =
if poly then Polymorphic_const_entry univs
- else Monomorphic_const_entry univs
+ else
+ (* FIXME be smarter about this *)
+ Monomorphic_const_entry (Univ.ContextSet.of_context univs)
in
{ const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
@@ -340,7 +342,7 @@ let dummy_inductive_entry (_,m) = ([],{
mind_entry_record = None;
mind_entry_finite = Decl_kinds.BiFinite;
mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
- mind_entry_universes = Monomorphic_ind_entry Univ.UContext.empty;
+ mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
mind_entry_private = None;
})
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index b95796fd8..d5312c500 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -63,7 +63,7 @@ type constant_def =
| OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
type constant_universes =
- | Monomorphic_const of Univ.UContext.t
+ | Monomorphic_const of Univ.ContextSet.t
| Polymorphic_const of Univ.AUContext.t
(** The [typing_flags] are instructions to the type-checker which
@@ -168,9 +168,9 @@ type one_inductive_body = {
}
type abstract_inductive_universes =
- | Monomorphic_ind of Univ.UContext.t
+ | Monomorphic_ind of Univ.ContextSet.t
| Polymorphic_ind of Univ.AUContext.t
- | Cumulative_ind of Univ.ACumulativityInfo.t
+ | Cumulative_ind of Univ.ACumulativityInfo.t
type mutual_inductive_body = {
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index f5c26b33d..d8768a0fc 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -126,7 +126,7 @@ let hcons_const_def = function
let hcons_const_universes cbu =
match cbu with
| Monomorphic_const ctx ->
- Monomorphic_const (Univ.hcons_universe_context ctx)
+ Monomorphic_const (Univ.hcons_universe_context_set ctx)
| Polymorphic_const ctx ->
Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
@@ -274,7 +274,7 @@ let hcons_mind_packet oib =
let hcons_mind_universes miu =
match miu with
- | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context ctx)
+ | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx)
| Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
| Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 185dba409..c44a17df2 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -35,9 +35,9 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
*)
type inductive_universes =
- | Monomorphic_ind_entry of Univ.UContext.t
+ | Monomorphic_ind_entry of Univ.ContextSet.t
| Polymorphic_ind_entry of Univ.UContext.t
- | Cumulative_ind_entry of Univ.CumulativityInfo.t
+ | Cumulative_ind_entry of Univ.CumulativityInfo.t
type one_inductive_entry = {
mind_entry_typename : Id.t;
@@ -65,9 +65,11 @@ type 'a proof_output = constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
type constant_universes_entry =
- | Monomorphic_const_entry of Univ.UContext.t
+ | Monomorphic_const_entry of Univ.ContextSet.t
| Polymorphic_const_entry of Univ.UContext.t
+type 'a in_constant_universes_entry = 'a * constant_universes_entry
+
type 'a definition_entry = {
const_entry_body : 'a const_entry_body;
(* List of section variables *)
@@ -82,7 +84,7 @@ type 'a definition_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Context.Named.t option * bool * types Univ.in_universe_context * inline
+ Context.Named.t option * types in_constant_universes_entry * inline
type projection_entry = {
proj_entry_ind : MutInd.t;
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 083b0ae40..8e9b606a5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -265,13 +265,12 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
(* Params are typed-checked here *)
- let univctx =
+ let env' =
match mie.mind_entry_universes with
- | Monomorphic_ind_entry ctx -> ctx
- | Polymorphic_ind_entry ctx -> ctx
- | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+ | Monomorphic_ind_entry ctx -> push_context_set ctx env
+ | Polymorphic_ind_entry ctx -> push_context ctx env
+ | Cumulative_ind_entry cumi -> push_context (Univ.CumulativityInfo.univ_context cumi) env
in
- let env' = push_context univctx env in
let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
(* We first type arity of each inductive definition *)
(* This allows building the environment of arities and to share *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8568bf14b..f7e755f00 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -79,18 +79,20 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
environment, because they do not appear in the type of the
definition. Any inconsistency will be raised at a later stage
when joining the environment. *)
- let env' = Environ.push_context ~strict:true ctx env' in
- let c',cst = match cb.const_body with
- | Undef _ | OpaqueDef _ ->
- let j = Typeops.infer env' c in
- let typ = cb.const_type in
- let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
- j.uj_type typ in
- j.uj_val, cst'
- | Def cs ->
- let c' = Mod_subst.force_constr cs in
- c, Reduction.infer_conv env' (Environ.universes env') c c'
- in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+ let env' = Environ.push_context ~strict:true ctx env' in
+ let c',cst = match cb.const_body with
+ | Undef _ | OpaqueDef _ ->
+ let j = Typeops.infer env' c in
+ let typ = cb.const_type in
+ let cst' = Reduction.infer_conv_leq env' (Environ.universes env')
+ j.uj_type typ in
+ j.uj_val, cst'
+ | Def cs ->
+ let c' = Mod_subst.force_constr cs in
+ c, Reduction.infer_conv env' (Environ.universes env') c c'
+ in
+ let ctx = Univ.ContextSet.of_context ctx in
+ c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
| Polymorphic_const uctx ->
let subst, ctx = Univ.abstract_universes ctx in
let c = Vars.subst_univs_level_constr subst c in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0e416b3e5..0e41bfc3c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -249,14 +249,14 @@ let universes_of_private eff =
in
match cb.const_universes with
| Monomorphic_const ctx ->
- (Univ.ContextSet.of_context ctx) :: acc
+ ctx :: acc
| Polymorphic_const _ -> acc
)
acc l
| Entries.SEsubproof (c, cb, e) ->
match cb.const_universes with
| Monomorphic_const ctx ->
- (Univ.ContextSet.of_context ctx) :: acc
+ ctx :: acc
| Polymorphic_const _ -> acc
)
[] (Term_typing.uniq_seff eff)
@@ -389,7 +389,6 @@ let push_named_def (id,de) senv =
| Monomorphic_const_entry _ -> false
| Polymorphic_const_entry _ -> true
in
- let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
| Def c -> Mod_subst.force_constr c, univs
| OpaqueDef o ->
@@ -425,9 +424,8 @@ let labels_of_mib mib =
let globalize_constant_universes env cb =
match cb.const_universes with
- | Monomorphic_const ctx ->
- let cstrs = Univ.ContextSet.of_context ctx in
- Now (false, cstrs) ::
+ | Monomorphic_const cstrs ->
+ Now (false, cstrs) ::
(match cb.const_body with
| (Undef _ | Def _) -> []
| OpaqueDef lc ->
@@ -443,7 +441,7 @@ let globalize_constant_universes env cb =
let globalize_mind_universes mb =
match mb.mind_universes with
| Monomorphic_ind ctx ->
- [Now (false, Univ.ContextSet.of_context ctx)]
+ [Now (false, ctx)]
| Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
| Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 4617f2d5f..70dd6438d 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,11 +125,10 @@ let inline_side_effects env body ctx side_eff =
| _ -> assert false
in
match cb.const_universes with
- | Monomorphic_const cnstctx ->
+ | Monomorphic_const univs ->
(** Abstract over the term at the top of the proof *)
let ty = cb.const_type in
let subst = Cmap_env.add c (Inr var) subst in
- let univs = Univ.ContextSet.of_context cnstctx in
let ctx = Univ.ContextSet.union ctx univs in
(subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
| Polymorphic_const auctx ->
@@ -228,19 +227,25 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes abstract uctx =
- if not abstract then
+let abstract_constant_universes abstract = function
+ | Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
- else
- let sbst, auctx = Univ.abstract_universes uctx in
- sbst, Polymorphic_const auctx
+ | Polymorphic_const_entry uctx ->
+ if not abstract then
+ Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
+ else
+ let sbst, auctx = Univ.abstract_universes uctx in
+ sbst, Polymorphic_const auctx
let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
match dcl with
- | ParameterEntry (ctx,poly,(t,uctx),nl) ->
- let env = push_context ~strict:(not poly) uctx env in
+ | ParameterEntry (ctx,(t,uctx),nl) ->
+ let env = match uctx with
+ | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
+ | Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
+ in
let j = infer env t in
- let abstract = poly && not (Option.is_empty kn) in
+ let abstract = not (Option.is_empty kn) in
let usubst, univs =
abstract_constant_universes abstract uctx
in
@@ -262,7 +267,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
const_entry_universes = Monomorphic_const_entry univs } as c) ->
- let env = push_context ~strict:true univs env in
+ let env = push_context_set ~strict:true univs env in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let tyj = infer_type env typ in
let proofterm =
@@ -301,21 +306,22 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
let { const_entry_type = typ; const_entry_opaque = opaque } = c in
let { const_entry_body = body; const_entry_feedback = feedback_id } = c in
let (body, ctx), side_eff = Future.join body in
- let poly, univs = match c.const_entry_universes with
+ let poly, univsctx = match c.const_entry_universes with
| Monomorphic_const_entry univs -> false, univs
- | Polymorphic_const_entry univs -> true, univs
+ | Polymorphic_const_entry univs -> true, Univ.ContextSet.of_context univs
in
- let univsctx = Univ.ContextSet.of_context univs in
let ctx = Univ.ContextSet.union univsctx ctx in
let body, ctx, _ = match trust with
| Pure -> body, ctx, []
| SideEffects _ -> inline_side_effects env body ctx side_eff
in
let env = push_context_set ~strict:(not poly) ctx env in
- let abstract = poly && not (Option.is_empty kn) in
- let usubst, univs =
- abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
- in
+ let abstract = not (Option.is_empty kn) in
+ let ctx = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+ else Monomorphic_const_entry ctx
+ in
+ let usubst, univs = abstract_constant_universes abstract ctx in
let j = infer env body in
let typ = match typ with
| None ->
@@ -556,7 +562,7 @@ let export_side_effects mb env ce =
let env = Environ.add_constant kn cb env in
match cb.const_universes with
| Monomorphic_const ctx ->
- Environ.push_context ~strict:true ctx env
+ Environ.push_context_set ~strict:true ctx env
| Polymorphic_const _ -> env
end
| kn, cb, `Opaque(_, ctx), _ ->
@@ -564,7 +570,7 @@ let export_side_effects mb env ce =
let env = Environ.add_constant kn cb env in
match cb.const_universes with
| Monomorphic_const cstctx ->
- let env = Environ.push_context ~strict:true cstctx env in
+ let env = Environ.push_context_set ~strict:true cstctx env in
Environ.push_context_set ~strict:true ctx env
| Polymorphic_const _ -> env
end
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 9b35bfc6e..55da4197e 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -19,7 +19,7 @@ type _ trust =
| SideEffects : structure_body -> side_effects trust
val translate_local_def : 'a trust -> env -> Id.t -> 'a definition_entry ->
- constant_def * types * Univ.UContext.t
+ constant_def * types * Univ.ContextSet.t
val translate_local_assum : env -> types -> types
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7fe4f8274..64afb95d5 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1053,6 +1053,7 @@ struct
let constraints (univs, cst) = cst
let levels (univs, cst) = univs
+ let size (univs,_) = LSet.cardinal univs
end
type universe_context_set = ContextSet.t
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 8d46a8bee..c06ce2446 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -310,7 +310,7 @@ sig
(** Keeps the order of the instances *)
val union : t -> t -> t
- (* the number of universes in the context *)
+ (** the number of universes in the context *)
val size : t -> int
end
@@ -423,6 +423,9 @@ sig
val constraints : t -> constraints
val levels : t -> LSet.t
+
+ (** the number of universes in the context *)
+ val size : t -> int
end
(** A set of universes with universe constraints.
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 0e452621c..578a89371 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -93,7 +93,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
let mib = Environ.lookup_mind mi env in
let ulen =
match mib.Declarations.mind_universes with
- | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+ | Declarations.Monomorphic_ind ctx -> Univ.ContextSet.size ctx
| Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
| Declarations.Cumulative_ind cumi ->
Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f6523d28c..a2f5a4577 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1972,9 +1972,13 @@ let add_morphism_infer glob m n =
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
if Lib.is_modtype () then
+ let uctx = if poly
+ then Entries.Polymorphic_const_entry (UState.context uctx)
+ else Entries.Monomorphic_const_entry (UState.context_set uctx)
+ in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
- (None,poly,(instance,UState.context uctx),None),
+ (None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8fc00ed96..b4ac94103 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -556,26 +556,26 @@ let print_constant with_values sep sp =
Vars.subst_instance_constr inst cb.const_type
in
let univs =
+ let open Entries in
let otab = Global.opaque_tables () in
match cb.const_body with
| Undef _ | Def _ ->
begin
match cb.const_universes with
- | Monomorphic_const ctx -> ctx
+ | Monomorphic_const ctx -> Monomorphic_const_entry ctx
| Polymorphic_const ctx ->
let inst = Univ.AUContext.instance ctx in
- Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+ Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
end
| OpaqueDef o ->
let body_uctxs = Opaqueproof.force_constraints otab o in
match cb.const_universes with
| Monomorphic_const ctx ->
- let uctxs = Univ.ContextSet.of_context ctx in
- Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+ Monomorphic_const_entry (Univ.ContextSet.union body_uctxs ctx)
| Polymorphic_const ctx ->
assert(Univ.ContextSet.is_empty body_uctxs);
let inst = Univ.AUContext.instance ctx in
- Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx)
+ Polymorphic_const_entry (Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx))
in
let ctx =
Evd.evar_universe_context_of_binders
@@ -589,12 +589,12 @@ let print_constant with_values sep sp =
str"*** [ " ++
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_universe_ctx sigma univs
+ Printer.pr_constant_universes sigma univs
| Some (c, ctx) ->
let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
- Printer.pr_universe_ctx sigma univs)
+ Printer.pr_constant_universes sigma univs)
let gallina_print_constant_with_infos sp =
print_constant true " = " sp ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 4d5cfcba3..ae6292024 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -270,6 +270,10 @@ let pr_universe_ctx sigma c =
else
mt()
+let pr_constant_universes sigma = function
+ | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx
+ | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx
+
let pr_cumulativity_info sigma cumi =
if !Detyping.print_universes
&& not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then
diff --git a/printing/printer.mli b/printing/printer.mli
index a3d0eaac2..67128da40 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -122,6 +122,7 @@ val pr_cumulative : bool -> bool -> Pp.t
val pr_universe_instance : evar_map -> Univ.UContext.t -> Pp.t
val pr_universe_ctx : evar_map -> Univ.UContext.t -> Pp.t
val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t
+val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t
val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t
(** Printing global references using names as short as possible *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index ea0408169..905173efc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -331,7 +331,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let initial_euctx = Proof.initial_euctx proof in
let fpl, univs = Future.split2 fpl in
let universes = if poly || now then Future.force univs else initial_euctx in
- let univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
+ let univctx = UState.check_univ_decl universes universe_decl in
let binders = if poly then Some (UState.universe_binders universes) else None in
(* Because of dependent subgoals at the beginning of proofs, we could
have existential variables in the initial types of goals, we need to
@@ -360,7 +360,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
the body. So we keep the two sets distinct. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx_body = UState.restrict ctx used_univs in
- let univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
+ let univs = UState.check_univ_decl ctx_body universe_decl in
(initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
else
(* Since the proof is computed now, we can simply have 1 set of
@@ -370,7 +370,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
TODO: check if restrict is really necessary now. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx = UState.restrict universes used_univs in
- let univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+ let univs = UState.check_univ_decl ctx universe_decl in
(univs, typ), ((body, Univ.ContextSet.empty), eff)
in
fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -383,7 +383,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
the declaration as well. If the declaration is non-extensible,
this will prevent the body from adding universes and constraints. *)
let bodyunivs = constrain_variables univctx (Future.force univs) in
- let univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
+ let univs = UState.check_univ_decl bodyunivs universe_decl in
(pt,Univ.ContextSet.of_context univs),eff)
in
let entry_fn p (_, t) =
@@ -392,7 +392,9 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let univs, typ = Future.force univstyp in
let univs =
if poly then Entries.Polymorphic_const_entry univs
- else Entries.Monomorphic_const_entry univs
+ else
+ (* FIXME be smarter about the unnecessary context linearisation in make_body *)
+ Entries.Monomorphic_const_entry (Univ.ContextSet.of_context univs)
in
{Entries.
const_entry_body = body;
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 92c326b1e..e1bf32f3c 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -123,10 +123,9 @@ 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 = UState.context ctx in
let univs =
- if p then Polymorphic_const_entry univs
- else Monomorphic_const_entry univs
+ if p then Polymorphic_const_entry (UState.context ctx)
+ else Monomorphic_const_entry (UState.context_set ctx)
in
let entry = {
const_entry_body =
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 1bacb7513..42fb52a3b 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -50,6 +50,6 @@ Type@{Top.17} -> Type@{v} -> Type@{u}
foo is universe polymorphic
Monomorphic mono = Type@{u}
: Type@{u+1}
-(* u |= *)
+(* {u} |= *)
mono is not universe polymorphic
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 6f5f96ee2..c99eba2cc 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -200,16 +200,22 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
let nf, subst = Evarutil.e_nf_evars_and_universes evars in
let termtype =
let t = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- nf t
- in
- Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
+ nf t
+ in
+ Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
let ctx = Evd.check_univ_decl !evars decl in
- let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
- (ParameterEntry
- (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
- in
+ let ctx = if poly
+ then Polymorphic_const_entry ctx
+ else
+ (* FIXME be smarter about this *)
+ Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
+ in
+ let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
+ (ParameterEntry
+ (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ in
Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
- instance_hook k pri global imps ?hook (ConstRef cst); id
+ instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
let props =
@@ -384,14 +390,20 @@ let context poly l =
let uctx = ref (Evd.universe_context_set !evars) in
let fn status (id, b, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
- let ctx = Univ.ContextSet.to_context !uctx in
(* Declare the universe context once *)
+ let univs = !uctx in
let () = uctx := Univ.ContextSet.empty in
let decl = match b with
| None ->
- (ParameterEntry (None,poly,(t,ctx),None), IsAssumption Logical)
+ let univs = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context univs)
+ else Monomorphic_const_entry univs
+ in
+ (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
| Some b ->
- let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ (* FIXME be smarter about this *)
+ let univs = Univ.ContextSet.to_context univs in
+ let entry = Declare.definition_entry ~poly ~univs ~types:t b in
(DefinitionEntry entry, IsAssumption Logical)
in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
diff --git a/vernac/command.ml b/vernac/command.ml
index 80599c534..06d0c8470 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -197,8 +197,11 @@ match local with
| DefaultInline -> Some (Flags.get_inline_level())
| InlineAt i -> Some i
in
- let ctx = Univ.ContextSet.to_context ctx in
- let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
+ let ctx = if p
+ then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
+ else Monomorphic_const_entry ctx
+ in
+ let decl = (ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
@@ -206,9 +209,9 @@ match local with
let () = assumption_message ident in
let () = Typeclasses.declare_instance None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
- let inst =
- if p (* polymorphic *) then Univ.UContext.instance ctx
- else Univ.Instance.empty
+ let inst = match ctx with
+ | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Monomorphic_const_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
@@ -606,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
else Polymorphic_ind_entry uctx
else
- Monomorphic_ind_entry uctx
+ Monomorphic_ind_entry (Univ.ContextSet.of_context uctx)
in
(* Build the mutual inductive entry *)
let mind_ent =
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c728c2671..e4ca98749 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -109,10 +109,10 @@ let _ =
let define id internal ctx c t =
let f = declare_constant ~internal in
- let univs = Evd.to_universe_context ctx in
let univs =
- if Flags.is_universe_polymorphism () then Polymorphic_const_entry univs
- else Monomorphic_const_entry univs
+ if Flags.is_universe_polymorphism ()
+ then Polymorphic_const_entry (Evd.to_universe_context ctx)
+ else Monomorphic_const_entry (Evd.universe_context_set ctx)
in
let kn = f id
(DefinitionEntry
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 71d80c4db..f59b5fcae 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -242,7 +242,11 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
| Global -> false
| Discharge -> assert false
in
- let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
+ let ctx = if p
+ then Polymorphic_const_entry ctx
+ else Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
+ in
+ let decl = (ParameterEntry (None,(t_i,ctx),None), k) in
let kn = declare_constant id ~local decl in
(locality,ConstRef kn,imps))
| Some body ->
@@ -491,9 +495,12 @@ let save_proof ?proof = function
if const_entry_type = None then
user_err Pp.(str "Admitted requires an explicit statement");
let typ = Option.get const_entry_type in
- let ctx = UState.context (fst universes) in
+ let ctx = if pi2 k (* polymorphic *)
+ then Polymorphic_const_entry (UState.context (fst universes))
+ else Monomorphic_const_entry (UState.context_set (fst universes))
+ in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
- Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
+ Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
| None ->
let pftree = Proof_global.give_me_the_proof () in
let id, k, typ = Pfedit.current_proof_statement () in
@@ -516,8 +523,12 @@ let save_proof ?proof = function
let evd = Evd.from_ctx universes in
let ctx = Evd.check_univ_decl evd decl in
let poly = pi2 k in
+ let ctx = if poly
+ then Polymorphic_const_entry ctx
+ else Monomorphic_const_entry (Univ.ContextSet.of_context ctx)
+ in
let binders = if poly then Some (UState.universe_binders universes) else None in
- Admitted(id,k,(sec_vars, poly, (typ, ctx), None),
+ Admitted(id,k,(sec_vars, (typ, ctx), None),
(universes, binders))
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 43af8968f..a9110c76c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -633,12 +633,11 @@ let declare_obligation prg obl body ty uctx =
shrink_body body ty else [], body, ty, [||]
in
let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
- let univs = if poly then Polymorphic_const_entry uctx else Monomorphic_const_entry uctx in
let ce =
{ const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
const_entry_secctx = None;
const_entry_type = ty;
- const_entry_universes = univs;
+ const_entry_universes = uctx;
const_entry_opaque = opaque;
const_entry_inline_code = false;
const_entry_feedback = None;
@@ -647,13 +646,15 @@ let declare_obligation prg obl body ty uctx =
let constant = Declare.declare_constant obl.obl_name ~local:true
(DefinitionEntry ce,IsProof Property)
in
- if not opaque then add_hint (Locality.make_section_locality None) prg constant;
- definition_message obl.obl_name;
- true, { obl with obl_body =
- if poly then
- Some (DefinedObl (constant, Univ.UContext.instance uctx))
- else
- Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx)) }
+ if not opaque then add_hint (Locality.make_section_locality None) prg constant;
+ definition_message obl.obl_name;
+ let body = match uctx with
+ | Polymorphic_const_entry uctx ->
+ Some (DefinedObl (constant, Univ.UContext.instance uctx))
+ | Monomorphic_const_entry _ ->
+ Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
+ in
+ true, { obl with obl_body = body }
let init_prog_info ?(opaque = false) sign n udecl b t ctx deps fixkind
notations obls impls kind reduce hook =
@@ -855,7 +856,10 @@ let obligation_terminator name num guard hook auto pf =
| (_, status), Vernacexpr.Transparent -> status
in
let obl = { obl with obl_status = false, status } in
- let uctx = UState.context ctx in
+ let uctx = if pi2 prg.prg_kind
+ then Polymorphic_const_entry (UState.context ctx)
+ else Monomorphic_const_entry (UState.context_set ctx)
+ in
let (_, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
@@ -967,13 +971,16 @@ and solve_obligation_by_tac prg obls i tac =
let evd = Evd.from_ctx prg.prg_ctx in
let evd = Evd.update_sigma_env evd (Global.env ()) in
let t, ty, ctx =
- solve_by_tac obl.obl_name (evar_of_obligation obl) tac
- (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
- in
- let uctx = UState.context ctx in
- let prg = {prg with prg_ctx = ctx} in
- let def, obl' = declare_obligation prg obl t ty uctx in
- obls.(i) <- obl';
+ solve_by_tac obl.obl_name (evar_of_obligation obl) tac
+ (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+ in
+ let uctx = if pi2 prg.prg_kind
+ then Polymorphic_const_entry (UState.context ctx)
+ else Monomorphic_const_entry (UState.context_set ctx)
+ in
+ let prg = {prg with prg_ctx = ctx} in
+ let def, obl' = declare_obligation prg obl t ty uctx in
+ obls.(i) <- obl';
if def && not (pi2 prg.prg_kind) then (
(* Declare the term constraints with the first obligation only *)
let evd = Evd.from_env (Global.env ()) in
@@ -1121,9 +1128,9 @@ let admit_prog prg =
match x.obl_body with
| None ->
let x = subst_deps_obl obls x in
- let ctx = UState.context prg.prg_ctx in
+ let ctx = Monomorphic_const_entry (UState.context_set prg.prg_ctx) in
let kn = Declare.declare_constant x.obl_name ~local:true
- (ParameterEntry (None,false,(x.obl_type,ctx),None), IsAssumption Conjectural)
+ (ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
in
assumption_message x.obl_name;
obls.(i) <- { x with obl_body = Some (DefinedObl (kn, Univ.Instance.empty)) }
diff --git a/vernac/record.ml b/vernac/record.ml
index 0819dadb4..faf277d86 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -270,7 +270,10 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
- let u = Univ.UContext.instance ctx in
+ let u = match ctx with
+ | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Monomorphic_const_entry ctx -> Univ.Instance.empty
+ in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
@@ -327,16 +330,12 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
- let univs =
- if poly then Polymorphic_const_entry ctx
- else Monomorphic_const_entry ctx
- in
let entry = {
const_entry_body =
Future.from_val (Safe_typing.mk_pure_proof proj);
const_entry_secctx = None;
const_entry_type = Some projtyp;
- const_entry_universes = univs;
+ const_entry_universes = ctx;
const_entry_opaque = false;
const_entry_inline_code = false;
const_entry_feedback = None } in
@@ -391,11 +390,14 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
let args = Context.Rel.to_extended_list mkRel nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
- let poly, ctx =
+ let template, ctx =
match univs with
- | Monomorphic_ind_entry ctx -> false, Univ.UContext.empty
- | Polymorphic_ind_entry ctx -> true, ctx
- | Cumulative_ind_entry cumi -> true, (Univ.CumulativityInfo.univ_context cumi)
+ | Monomorphic_ind_entry ctx ->
+ template, Monomorphic_const_entry Univ.ContextSet.empty
+ | Polymorphic_ind_entry ctx ->
+ false, Polymorphic_const_entry ctx
+ | Cumulative_ind_entry cumi ->
+ false, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -405,7 +407,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
let mie_ind =
{ mind_entry_typename = id;
mind_entry_arity = arity;
- mind_entry_template = not poly && template;
+ mind_entry_template = template;
mind_entry_consnames = [idbuild];
mind_entry_lc = [type_constructor] }
in
@@ -419,14 +421,13 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
}
in
let mie =
- if poly then
- begin
+ match ctx with
+ | Polymorphic_const_entry ctx ->
let env = Global.env () in
let env' = Environ.push_context ctx env in
let evd = Evd.from_env env' in
Inductiveops.infer_inductive_subtyping env' evd mie
- end
- else
+ | Monomorphic_const_entry _ ->
mie
in
let kn = Command.declare_mutual_inductive_with_eliminations mie ubinders [(paramimpls,[])] in
@@ -434,6 +435,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
let cstr = (rsp,1) in
let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name coers ubinders fieldimpls fields in
let build = ConstructRef cstr in
+ let poly = match ctx with | Polymorphic_const_entry _ -> true | Monomorphic_const_entry _ -> false in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs);
rsp
@@ -499,7 +501,7 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
else
Polymorphic_ind_entry ctx
else
- Monomorphic_ind_entry ctx
+ Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
in
let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
@@ -626,7 +628,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
else
Polymorphic_ind_entry ctx
else
- Monomorphic_ind_entry ctx
+ Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
in
let ind = declare_structure finite pl univs idstruc
idbuild implpars params arity template implfs
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 16:09:31 +0000