aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli11
-rw-r--r--engine/evd.ml5
-rw-r--r--engine/evd.mli8
-rw-r--r--engine/uState.ml107
-rw-r--r--engine/uState.mli17
-rw-r--r--interp/declare.ml13
-rw-r--r--interp/declare.mli6
-rw-r--r--plugins/funind/functional_principles_types.ml7
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/ltac/extratactics.ml46
-rw-r--r--plugins/ltac/rewrite.ml9
-rw-r--r--plugins/setoid_ring/newring.ml10
-rw-r--r--proofs/proof_global.ml31
-rw-r--r--tactics/leminv.ml11
-rw-r--r--vernac/class.ml4
-rw-r--r--vernac/classes.ml34
-rw-r--r--vernac/command.ml44
-rw-r--r--vernac/declareDef.ml4
-rw-r--r--vernac/declareDef.mli7
-rw-r--r--vernac/lemmas.ml36
-rw-r--r--vernac/obligations.ml17
-rw-r--r--vernac/record.ml54
22 files changed, 251 insertions, 198 deletions
diff --git a/API/API.mli b/API/API.mli
index ad5d5490b..4405bf8da 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -2764,6 +2764,9 @@ sig
val context_set : t -> Univ.ContextSet.t
val of_context_set : Univ.ContextSet.t -> t
+ val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+ val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
+
type rigid =
| UnivRigid
| UnivFlexible of bool
@@ -2887,6 +2890,8 @@ sig
val from_ctx : UState.t -> evar_map
val to_universe_context : evar_map -> Univ.UContext.t
+ val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+ val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
val meta_list : evar_map -> (Constr.metavariable * clbinding) list
@@ -4669,11 +4674,11 @@ sig
val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:Decl_kinds.definition_object_kind ->
- ?local:bool -> ?poly:Decl_kinds.polymorphic -> Names.Id.t -> ?types:Constr.t ->
- Constr.t Univ.in_universe_context_set -> Names.Constant.t
+ ?local:bool -> Names.Id.t -> ?types:Constr.t ->
+ Constr.t Entries.in_constant_universes_entry -> Names.Constant.t
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:Constr.types ->
- ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t ->
+ ?univs:Entries.constant_universes_entry ->
?eff:Safe_typing.private_constants -> Constr.t -> Safe_typing.private_constants Entries.definition_entry
val definition_message : Names.Id.t -> unit
val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name
diff --git a/engine/evd.ml b/engine/evd.ml
index eb0f2e3e7..9ea2cc00f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -758,7 +758,10 @@ let universe_context_set d = UState.context_set d.universes
let to_universe_context evd = UState.context evd.universes
-let check_univ_decl evd decl = UState.check_univ_decl evd.universes decl
+let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
+let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+
+let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
let restrict_universe_context evd vars =
{ evd with universes = UState.restrict evd.universes vars }
diff --git a/engine/evd.mli b/engine/evd.mli
index 49b6a7583..f06fb8d3b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -562,8 +562,12 @@ val universes : evar_map -> UGraph.t
[Univ.ContextSet.to_context]. *)
val to_universe_context : evar_map -> Univ.UContext.t
-val check_univ_decl : evar_map -> UState.universe_decl ->
- Univ.UContext.t
+val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+
+(** NB: [ind_univ_entry] cannot create cumulative entries. *)
+val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
val merge_universe_context : evar_map -> UState.t -> evar_map
val set_universe_context : evar_map -> UState.t -> evar_map
diff --git a/engine/uState.ml b/engine/uState.ml
index ff91493ee..dadc004c5 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -87,6 +87,17 @@ let constraints ctx = snd ctx.uctx_local
let context ctx = Univ.ContextSet.to_context ctx.uctx_local
+let const_univ_entry ~poly uctx =
+ let open Entries in
+ if poly then Polymorphic_const_entry (context uctx)
+ else Monomorphic_const_entry (context_set uctx)
+
+(* does not support cumulativity since you need more info *)
+let ind_univ_entry ~poly uctx =
+ let open Entries in
+ if poly then Polymorphic_ind_entry (context uctx)
+ else Monomorphic_ind_entry (context_set uctx)
+
let of_context_set ctx = { empty with uctx_local = ctx }
let subst ctx = ctx.uctx_univ_variables
@@ -260,58 +271,92 @@ let pr_uctx_level uctx =
type universe_decl =
(Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+let error_unbound_universes left uctx =
+ let open Univ in
+ let n = LSet.cardinal left in
+ let loc =
+ try
+ let info =
+ LMap.find (LSet.choose left) (snd uctx.uctx_names) in
+ info.uloc
+ with Not_found -> None
+ in
+ user_err ?loc ~hdr:"universe_context"
+ ((str(CString.plural n "Universe") ++ spc () ++
+ LSet.pr (pr_uctx_level uctx) left ++
+ spc () ++ str (CString.conjugate_verb_to_be n) ++
+ str" unbound."))
+
let universe_context ~names ~extensible uctx =
- let levels = Univ.ContextSet.levels uctx.uctx_local in
+ let open Univ in
+ let levels = ContextSet.levels uctx.uctx_local in
let newinst, left =
List.fold_right
(fun (loc,id) (newinst, acc) ->
let l =
try UNameMap.find id (fst uctx.uctx_names)
- with Not_found ->
- user_err ?loc ~hdr:"universe_context"
- (str"Universe " ++ Id.print id ++ str" is not bound anymore.")
- in (l :: newinst, Univ.LSet.remove l acc))
+ with Not_found -> assert false
+ in (l :: newinst, LSet.remove l acc))
names ([], levels)
in
- if not extensible && not (Univ.LSet.is_empty left) then
- let n = Univ.LSet.cardinal left in
- let loc =
- try
- let info =
- Univ.LMap.find (Univ.LSet.choose left) (snd uctx.uctx_names) in
- info.uloc
- with Not_found -> None
- in
- user_err ?loc ~hdr:"universe_context"
- ((str(CString.plural n "Universe") ++ spc () ++
- Univ.LSet.pr (pr_uctx_level uctx) left ++
- spc () ++ str (CString.conjugate_verb_to_be n) ++
- str" unbound."))
+ if not extensible && not (LSet.is_empty left)
+ then error_unbound_universes left uctx
else
- let left = Univ.ContextSet.sort_levels (Array.of_list (Univ.LSet.elements left)) in
+ let left = ContextSet.sort_levels (Array.of_list (LSet.elements left)) in
let inst = Array.append (Array.of_list newinst) left in
- let inst = Univ.Instance.of_array inst in
- let ctx = Univ.UContext.make (inst,
- Univ.ContextSet.constraints uctx.uctx_local) in
+ let inst = Instance.of_array inst in
+ let ctx = UContext.make (inst, ContextSet.constraints uctx.uctx_local) in
ctx
-let check_implication uctx cstrs ctx =
+let check_universe_context_set ~names ~extensible uctx =
+ if extensible then ()
+ else
+ let open Univ in
+ let left = List.fold_left (fun left (loc,id) ->
+ let l =
+ try UNameMap.find id (fst uctx.uctx_names)
+ with Not_found -> assert false
+ in LSet.remove l left)
+ (ContextSet.levels uctx.uctx_local) names
+ in
+ if not (LSet.is_empty left)
+ then error_unbound_universes left uctx
+
+let check_implication uctx cstrs cstrs' =
let gr = initial_graph uctx in
let grext = UGraph.merge_constraints cstrs gr in
- let cstrs' = Univ.UContext.constraints ctx in
if UGraph.check_constraints cstrs' grext then ()
else CErrors.user_err ~hdr:"check_univ_decl"
(str "Universe constraints are not implied by the ones declared.")
-let check_univ_decl uctx decl =
+let check_mono_univ_decl uctx decl =
+ let open Misctypes in
+ let () =
+ let names = decl.univdecl_instance in
+ let extensible = decl.univdecl_extensible_instance in
+ check_universe_context_set ~names ~extensible uctx
+ in
+ if not decl.univdecl_extensible_constraints then
+ check_implication uctx
+ decl.univdecl_constraints
+ (Univ.ContextSet.constraints uctx.uctx_local);
+ uctx.uctx_local
+
+let check_univ_decl ~poly uctx decl =
let open Misctypes in
- let ctx = universe_context
- ~names:decl.univdecl_instance
- ~extensible:decl.univdecl_extensible_instance
- uctx
+ let ctx =
+ let names = decl.univdecl_instance in
+ let extensible = decl.univdecl_extensible_instance in
+ if poly
+ then Entries.Polymorphic_const_entry (universe_context ~names ~extensible uctx)
+ else
+ let () = check_universe_context_set ~names ~extensible uctx in
+ Entries.Monomorphic_const_entry uctx.uctx_local
in
if not decl.univdecl_extensible_constraints then
- check_implication uctx decl.univdecl_constraints ctx;
+ check_implication uctx
+ decl.univdecl_constraints
+ (Univ.ContextSet.constraints uctx.uctx_local);
ctx
let restrict ctx vars =
diff --git a/engine/uState.mli b/engine/uState.mli
index 5279c6388..4265f2b20 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -59,6 +59,13 @@ val constraints : t -> Univ.constraints
val context : t -> Univ.UContext.t
(** Shorthand for {!context_set} with {!Context_set.to_context}. *)
+val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+(** Pick from {!context} or {!context_set} based on [poly]. *)
+
+val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
+(** Pick from {!context} or {!context_set} based on [poly].
+ Cannot create cumulative entries. *)
+
(** {5 Constraints handling} *)
val add_constraints : t -> Univ.constraints -> t
@@ -133,11 +140,15 @@ type universe_decl =
If non extensible in [decl], check that the local universes (resp.
universe constraints) in [ctx] are implied by [decl].
- Return a universe context containing the local universes of [ctx]
- and their constraints. The universes corresponding to
+ Return a [Entries.constant_universes_entry] containing the local
+ universes of [ctx] and their constraints.
+
+ When polymorphic, the universes corresponding to
[decl.univdecl_instance] come first in the order defined by that
list. *)
-val check_univ_decl : t -> universe_decl -> Univ.UContext.t
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+
+val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
(** {5 TODO: Document me} *)
diff --git a/interp/declare.ml b/interp/declare.ml
index 15999f1d1..1b4645aff 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -203,14 +203,9 @@ let declare_constant_common id cst =
update_tables c;
c
+let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
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
- (* FIXME be smarter about this *)
- Monomorphic_const_entry (Univ.ContextSet.of_context univs)
- in
+ ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
{ const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
const_entry_secctx = None;
const_entry_type = types;
@@ -263,9 +258,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
let declare_definition ?(internal=UserIndividualRequest)
?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
- ?(poly=false) id ?types (body,ctx) =
+ id ?types (body,univs) =
let cb =
- definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
+ definition_entry ?types ~univs ~opaque body
in
declare_constant ~internal ~local id
(Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
diff --git a/interp/declare.mli b/interp/declare.mli
index 9b3194dec..d50d37368 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -42,7 +42,7 @@ type internal_flag =
(* Defaut definition entries, transparent with no secctx or proj information *)
val definition_entry : ?fix_exn:Future.fix_exn ->
?opaque:bool -> ?inline:bool -> ?types:types ->
- ?poly:polymorphic -> ?univs:Univ.UContext.t ->
+ ?univs:Entries.constant_universes_entry ->
?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
(** [declare_constant id cd] declares a global declaration
@@ -56,8 +56,8 @@ val declare_constant :
val declare_definition :
?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
- ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr ->
- constr Univ.in_universe_context_set -> Constant.t
+ ?local:bool -> Id.t -> ?types:constr ->
+ constr Entries.in_constant_universes_entry -> Constant.t
(** Since transparent constants' side effects are globally declared, we
* need that *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 076fba861..7a9bbd92c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -348,8 +348,11 @@ let generate_functional_principle (evd: Evd.evar_map ref)
let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr value)) in
(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
- let univs = Evd.to_universe_context evd' in
- let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs value in
+ let univs =
+ let poly = Flags.is_universe_polymorphism () in
+ Evd.const_univ_entry ~poly evd'
+ in
+ let ce = Declare.definition_entry ~univs value in
ignore(
Declare.declare_constant
name
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 320f7c7f3..b0a76137b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -66,8 +66,8 @@ let find_reference sl s =
let dp = Names.DirPath.make (List.rev_map Id.of_string sl) in
locate (make_qualid dp (Id.of_string s))
-let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value =
- let ce = definition_entry ~univs:ctx value (*FIXME *) in
+let declare_fun f_id kind ?univs value =
+ let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
@@ -1556,8 +1556,8 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let functional_id = add_suffix function_name "_F" in
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
- let ctx = Evd.to_universe_context evm in
- declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx res
+ let univs = Entries.Monomorphic_const_entry (Evd.universe_context_set evm) in
+ declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
let evm = Evd.from_env (Global.env ()) in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d6cfa3cf9..750517e91 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -313,10 +313,10 @@ let project_hint pri l2r r =
let id =
Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l"))
in
- let ctx = Evd.universe_context_set sigma in
- let c = EConstr.to_constr sigma c in
let poly = Flags.use_polymorphic_flag () in
- let c = Declare.declare_definition ~poly ~internal:Declare.InternalTacticRequest id (c,ctx) in
+ let ctx = Evd.const_univ_entry ~poly sigma in
+ let c = EConstr.to_constr sigma c in
+ let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
(info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index a2f5a4577..c0060c5a7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1884,11 +1884,11 @@ let declare_projection n instance_id r =
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
- let ctx = Evd.to_universe_context sigma in
+ let univs = Evd.const_univ_entry ~poly sigma in
let typ = EConstr.to_constr sigma typ in
let term = EConstr.to_constr sigma term in
let cst =
- Declare.definition_entry ~types:typ ~poly ~univs:ctx term
+ Declare.definition_entry ~types:typ ~univs term
in
ignore(Declare.declare_constant n
(Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
@@ -1972,10 +1972,7 @@ 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 uctx = UState.const_univ_entry ~poly uctx in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
(None,(instance,uctx),None),
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 6d0b6fd09..f22f00839 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -150,13 +150,13 @@ let ic_unsafe c = (*FIXME remove *)
let sigma = Evd.from_env env in
EConstr.of_constr (fst (Constrintern.interp_constr env sigma c))
-let decl_constant na ctx c =
+let decl_constant na univs c =
let open Constr in
let vars = Univops.universes_of_constr c in
- let ctx = Univops.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in
+ let univs = Univops.restrict_universe_context univs vars in
+ let univs = Monomorphic_const_entry univs in
mkConst(declare_constant (Id.of_string na)
- (DefinitionEntry (definition_entry ~opaque:true
- ~univs:(Univ.ContextSet.to_context ctx) c),
+ (DefinitionEntry (definition_entry ~opaque:true ~univs c),
IsProof Lemma))
(* Calling a global tactic *)
@@ -220,7 +220,7 @@ let exec_tactic env evd n f args =
let gls = Proofview.V82.of_tactic (Tacinterp.eval_tactic_ist ist (ltac_call f (args@[getter]))) gl in
let evd, nf = Evarutil.nf_evars_and_universes (Refiner.project gls) in
let nf c = nf (constr_of c) in
- Array.map nf !tactic_res, Evd.to_universe_context evd
+ Array.map nf !tactic_res, Evd.universe_context_set evd
let stdlib_modules =
[["Coq";"Setoids";"Setoid"];
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 905173efc..bfd64e21b 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -316,10 +316,6 @@ let get_open_goals () =
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
List.length shelf
-let constrain_variables init uctx =
- let levels = Univ.Instance.levels (Univ.UContext.instance init) in
- UState.constrain_variables levels uctx
-
type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t
let close_proof ~keep_body_ucst_separate ?feedback_id ~now
@@ -329,9 +325,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let poly = pi2 strength (* Polymorphic *) in
let initial_goals = Proof.initial_goals proof in
let initial_euctx = Proof.initial_euctx proof in
+ let constrain_variables ctx =
+ UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+ in
let fpl, univs = Future.split2 fpl in
let universes = if poly || now then Future.force univs else initial_euctx in
- let univctx = UState.check_univ_decl universes universe_decl in
+ let univctx = UState.check_univ_decl ~poly 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
@@ -353,15 +352,15 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let used_univs_typ = Univops.universes_of_constr typ in
if keep_body_ucst_separate ||
not (Safe_typing.empty_private_constants = eff) then
- let initunivs = UState.context initial_euctx in
- let ctx = constrain_variables initunivs universes in
+ let initunivs = UState.const_univ_entry ~poly initial_euctx in
+ let ctx = constrain_variables universes in
(* For vi2vo compilation proofs are computed now but we need to
complement the univ constraints of the typ with the ones of
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 = UState.check_univ_decl ctx_body universe_decl in
- (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
+ let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+ (initunivs, typ), ((body, univs), eff)
else
(* Since the proof is computed now, we can simply have 1 set of
constraints in which we merge the ones for the body and the ones
@@ -370,7 +369,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 = UState.check_univ_decl ctx universe_decl in
+ let univs = UState.check_univ_decl ~poly ctx universe_decl in
(univs, typ), ((body, Univ.ContextSet.empty), eff)
in
fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -382,20 +381,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
the initial universes, ensure that the final universes respect
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 = UState.check_univ_decl bodyunivs universe_decl in
- (pt,Univ.ContextSet.of_context univs),eff)
+ let bodyunivs = constrain_variables (Future.force univs) in
+ let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+ (pt,univs),eff)
in
let entry_fn p (_, t) =
let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
let univs, typ = Future.force univstyp in
- let univs =
- if poly then Entries.Polymorphic_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;
const_entry_secctx = section_vars;
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 1ee873e0f..1ae3577ed 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -232,12 +232,15 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let invProof = it_mkNamedLambda_or_LetIn c !ownSign in
let invProof = EConstr.Unsafe.to_constr invProof in
let p = Evarutil.nf_evars_universes sigma invProof in
- p, Evd.to_universe_context sigma
+ p, sigma
let add_inversion_lemma name env sigma t sort dep inv_op =
- let invProof, univs = inversion_scheme env sigma t sort dep inv_op in
- let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
- ~univs invProof in
+ let invProof, sigma = inversion_scheme env sigma t sort dep inv_op in
+ let univs =
+ let poly = Flags.use_polymorphic_flag () in
+ Evd.const_univ_entry ~poly sigma
+ in
+ let entry = definition_entry ~univs invProof in
let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
()
diff --git a/vernac/class.ml b/vernac/class.ml
index 68fd22cb6..943da8fa8 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -212,10 +212,10 @@ let build_id_coercion idf_opt source poly =
Id.of_string ("Id_"^(ident_key_of_class source)^"_"^
(ident_key_of_class cl))
in
- let univs = Evd.to_universe_context sigma in
+ let univs = Evd.const_univ_entry ~poly sigma in
let constr_entry = (* Cast is necessary to express [val_f] is identity *)
DefinitionEntry
- (definition_entry ~types:typ_f ~poly ~univs
+ (definition_entry ~types:typ_f ~univs
~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
in
let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c99eba2cc..1833b7a1d 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -119,9 +119,9 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
(Univops.universes_of_constr term) in
Evd.restrict_universe_context evm levels
in
- let uctx = Evd.check_univ_decl evm decl in
+ let uctx = Evd.check_univ_decl ~poly evm decl in
let entry =
- Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+ Declare.definition_entry ~types:termtype ~univs:uctx term
in
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
@@ -203,16 +203,10 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
nf t
in
Pretyping.check_evars env Evd.empty !evars (EConstr.of_constr termtype);
- let ctx = Evd.check_univ_decl !evars decl 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 univs = Evd.check_univ_decl ~poly !evars decl in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
(ParameterEntry
- (None,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+ (None,(termtype,univs),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
@@ -391,19 +385,16 @@ let context poly l =
let fn status (id, b, t) =
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
(* Declare the universe context once *)
- let univs = !uctx in
+ let univs = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+ else Monomorphic_const_entry !uctx
+ in
let () = uctx := Univ.ContextSet.empty in
let decl = match b with
| None ->
- 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 ->
- (* FIXME be smarter about this *)
- let univs = Univ.ContextSet.to_context univs in
- let entry = Declare.definition_entry ~poly ~univs ~types:t b in
+ let entry = Declare.definition_entry ~univs ~types:t b in
(DefinitionEntry entry, IsAssumption Logical)
in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
@@ -426,9 +417,12 @@ let context poly l =
pi3 (Command.declare_assumption false decl (t, !uctx) Universes.empty_binders [] impl
Vernacexpr.NoInline (Loc.tag id))
| Some b ->
- let ctx = Univ.ContextSet.to_context !uctx in
+ let univs = if poly
+ then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx)
+ else Monomorphic_const_entry !uctx
+ in
let decl = (Discharge, poly, Definition) in
- let entry = Declare.definition_entry ~poly ~univs:ctx ~types:t b in
+ let entry = Declare.definition_entry ~univs ~types:t b in
let hook = Lemmas.mk_hook (fun _ gr -> gr) in
let _ = DeclareDef.declare_definition id decl entry Universes.empty_binders [] hook in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
diff --git a/vernac/command.ml b/vernac/command.ml
index 06d0c8470..1a8b16a89 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -88,7 +88,7 @@ let warn_implicits_in_term =
strbrk "Implicit arguments declaration relies on type." ++ spc () ++
strbrk "The term declares more implicits than the type here.")
-let interp_definition pl bl p red_option c ctypopt =
+let interp_definition pl bl poly red_option c ctypopt =
let env = Global.env() in
let evd, decl = Univdecls.interp_univ_decl_opt env pl in
let evdref = ref evd in
@@ -105,15 +105,15 @@ let interp_definition pl bl p red_option c ctypopt =
let c = EConstr.Unsafe.to_constr c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
let body = nf (it_mkLambda_or_LetIn c ctx) in
- let vars = Univops.universes_of_constr body in
- let evd = Evd.restrict_universe_context !evdref vars in
- let uctx = Evd.check_univ_decl evd decl in
+ let vars = Univops.universes_of_constr body in
+ let evd = Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly evd decl in
let binders = Evd.universe_binders evd in
imps1@(Impargs.lift_implicits nb_args imps2), binders,
- definition_entry ~univs:uctx ~poly:p body
+ definition_entry ~univs:uctx body
| Some ctyp ->
- let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
- let subst = evd_comb0 Evd.nf_univ_variables evdref in
+ let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
+ let subst = evd_comb0 Evd.nf_univ_variables evdref in
let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
@@ -134,10 +134,10 @@ let interp_definition pl bl p red_option c ctypopt =
let vars = Univ.LSet.union (Univops.universes_of_constr body)
(Univops.universes_of_constr typ) in
let ctx = Evd.restrict_universe_context !evdref vars in
- let uctx = Evd.check_univ_decl ctx decl in
+ let uctx = Evd.check_univ_decl ~poly ctx decl in
let binders = Evd.universe_binders evd in
imps1@(Impargs.lift_implicits nb_args impsty), binders,
- definition_entry ~types:typ ~poly:p
+ definition_entry ~types:typ
~univs:uctx body
in
red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
@@ -282,9 +282,14 @@ let do_assumptions_bound_univs coe kind nl id pl c =
let ty = nf ty in
let vars = Univops.universes_of_constr ty in
let evd = Evd.restrict_universe_context !evdref vars in
- let uctx = Evd.check_univ_decl evd decl in
+ let uctx = Evd.check_univ_decl ~poly:(pi2 kind) evd decl in
let binders = Evd.universe_binders evd in
- let uctx = Univ.ContextSet.of_context uctx in
+ let uctx = match uctx with
+ | Polymorphic_const_entry uctx ->
+ (* ?? *)
+ Univ.ContextSet.of_context uctx
+ | Monomorphic_const_entry uctx -> uctx
+ in
let (_, _, st) = declare_assumption coe kind (ty, uctx) binders impls false nl id in
st
@@ -582,7 +587,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
- let uctx = Evd.check_univ_decl evd decl in
+ let uctx = Evd.check_univ_decl ~poly evd decl in
List.iter (fun c -> check_evars env_params Evd.empty evd (EConstr.of_constr c)) arities;
Context.Rel.iter (fun c -> check_evars env0 Evd.empty evd (EConstr.of_constr c)) ctx_params;
List.iter (fun (_,ctyps,_) ->
@@ -604,12 +609,13 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
in
let univs =
- if poly then
+ match uctx with
+ | Polymorphic_const_entry uctx ->
if cum then
Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context uctx)
else Polymorphic_ind_entry uctx
- else
- Monomorphic_ind_entry (Univ.ContextSet.of_context uctx)
+ | Monomorphic_const_entry uctx ->
+ Monomorphic_ind_entry uctx
in
(* Build the mutual inductive entry *)
let mind_ent =
@@ -1032,9 +1038,9 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
let body = it_mkLambda_or_LetIn (mkApp (Evarutil.e_new_global evdref gr, [|make|])) binders_rel in
let ty = it_mkProd_or_LetIn top_arity binders_rel in
let ty = EConstr.Unsafe.to_constr ty in
- let univs = Evd.check_univ_decl !evdref decl in
+ let univs = Evd.check_univ_decl ~poly !evdref decl in
(*FIXME poly? *)
- let ce = definition_entry ~poly ~types:ty ~univs (EConstr.to_constr !evdref body) in
+ let ce = definition_entry ~types:ty ~univs (EConstr.to_constr !evdref body) in
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
@@ -1173,7 +1179,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
- let ctx = Evd.check_univ_decl evd pl in
+ let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
@@ -1206,7 +1212,7 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
let evd = Evd.from_ctx ctx in
let evd = Evd.restrict_universe_context evd vars in
- let ctx = Evd.check_univ_decl evd pl in
+ let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index c18744052..980db4109 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -57,7 +57,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
declare_global_definition ident ce local k pl imps in
Lemmas.call_hook fix_exn hook local r
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
- let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+ let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 01a87818a..55f7c7861 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -15,5 +15,8 @@ val declare_definition : Id.t -> definition_kind ->
Safe_typing.private_constants Entries.definition_entry -> Universes.universe_binders -> Impargs.manual_implicits ->
Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference
-val declare_fix : ?opaque:bool -> definition_kind -> Universes.universe_binders -> Univ.UContext.t -> Id.t ->
- Safe_typing.private_constants Entries.proof_output -> Constr.types -> Impargs.manual_implicits -> Globnames.global_reference
+val declare_fix : ?opaque:bool -> definition_kind ->
+ Universes.universe_binders -> Entries.constant_universes_entry ->
+ Id.t -> Safe_typing.private_constants Entries.proof_output ->
+ Constr.types -> Impargs.manual_implicits ->
+ Globnames.global_reference
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index f59b5fcae..a787ec6fa 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -224,7 +224,7 @@ let compute_proof_name locality = function
let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in
next_global_ident_away default_thm_id avoid
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,imps))) =
+let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
let t_i = norm t_i in
match body with
| None ->
@@ -232,7 +232,13 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let k = IsAssumption Conjectural in
- let c = SectionLocalAssum ((t_i,Univ.ContextSet.of_context ctx),p,impl) in
+ let univs = match univs with
+ | Polymorphic_const_entry univs ->
+ (* What is going on here? *)
+ Univ.ContextSet.of_context univs
+ | Monomorphic_const_entry univs -> univs
+ in
+ let c = SectionLocalAssum ((t_i, univs),p,impl) in
let _ = declare_variable id (Lib.cwd(),c,k) in
(Discharge, VarRef id,imps)
| Local | Global ->
@@ -242,11 +248,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
| Global -> false
| Discharge -> assert false
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 decl = (ParameterEntry (None,(t_i,univs),None), k) in
let kn = declare_constant id ~local decl in
(locality,ConstRef kn,imps))
| Some body ->
@@ -264,8 +266,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
let body_i = body_i body in
match locality with
| Discharge ->
- let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p
- ~univs:ctx body_i in
+ let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
(Discharge,VarRef id,imps)
@@ -276,7 +277,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i (id,(t_i,(_,im
| Discharge -> assert false
in
let const =
- Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
+ Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
in
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality,ConstRef kn,imps)
@@ -425,7 +426,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
let body,opaq = retrieve_first_recthm ctx ref in
let subst = Evd.evar_universe_context_subst ctx in
let norm c = Universes.subst_opt_univs_constr subst c in
- let ctx = UState.check_univ_decl ctx decl in
+ let ctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
let body = Option.map norm body in
List.map_i (save_remaining_recthms kind norm ctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
@@ -460,7 +461,7 @@ let start_proof_com ?inference_hook kind thms hook =
let () =
let open Misctypes in
if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
- ignore (Evd.check_univ_decl evd decl)
+ ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
in
let evd =
if pi2 kind then evd
@@ -495,10 +496,7 @@ 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 = if pi2 k (* polymorphic *)
- then Polymorphic_const_entry (UState.context (fst universes))
- else Monomorphic_const_entry (UState.context_set (fst universes))
- in
+ let ctx = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
| None ->
@@ -521,12 +519,8 @@ let save_proof ?proof = function
| _ -> None in
let decl = Proof_global.get_universe_decl () in
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 ctx = Evd.check_univ_decl ~poly evd decl in
let binders = if poly then Some (UState.universe_binders universes) else None in
Admitted(id,k,(sec_vars, (typ, ctx), None),
(universes, binders))
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a9110c76c..97cdd7977 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -475,12 +475,8 @@ let declare_definition prg =
(Evd.evar_universe_context_subst prg.prg_ctx) in
let opaque = prg.prg_opaque in
let fix_exn = Hook.get get_fix_exn () in
- let () = ignore(UState.check_univ_decl prg.prg_ctx prg.prg_univdecl) in
- let ce =
- definition_entry ~fix_exn
- ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
- ~univs:(UState.context prg.prg_ctx) (nf body)
- in
+ let univs = UState.check_univ_decl ~poly:(pi2 prg.prg_kind) prg.prg_ctx prg.prg_univdecl in
+ let ce = definition_entry ~fix_exn ~opaque ~types:(nf typ) ~univs (nf body) in
let () = progmap_remove prg in
let ubinders = UState.universe_binders prg.prg_ctx in
DeclareDef.declare_definition prg.prg_name
@@ -549,9 +545,9 @@ let declare_mutual_definition l =
mk_proof (mkCoFix (i,fixdecls))) 0 l
in
(* Declare the recursive definitions *)
- let ctx = UState.context first.prg_ctx in
+ let univs = UState.const_univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders ctx)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) Universes.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -856,10 +852,7 @@ 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 = if pi2 prg.prg_kind
- then Polymorphic_const_entry (UState.context ctx)
- else Monomorphic_const_entry (UState.context_set ctx)
- in
+ let uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
let (_, obl) = declare_obligation prg obl body ty uctx in
let obls = Array.copy obls in
let _ = obls.(num) <- obl in
diff --git a/vernac/record.ml b/vernac/record.ml
index faf277d86..1d255b08e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -95,7 +95,7 @@ let binder_of_decl = function
let binders_of_decls = List.map binder_of_decl
-let typecheck_params_and_fields finite def id pl t ps nots fs =
+let typecheck_params_and_fields finite def id poly pl t ps nots fs =
let env0 = Global.env () in
let evd, decl = Univdecls.interp_univ_decl_opt env0 pl in
let evars = ref evd in
@@ -167,7 +167,7 @@ let typecheck_params_and_fields finite def id pl t ps nots fs =
let newps = List.map (EConstr.to_rel_decl evars) newps in
let typ = EConstr.to_constr evars typ in
let ce t = Pretyping.check_evars env0 Evd.empty evars (EConstr.of_constr t) in
- let univs = Evd.check_univ_decl evars decl in
+ let univs = Evd.check_univ_decl ~poly evars decl in
let ubinders = Evd.universe_binders evars in
List.iter (iter_constr ce) (List.rev newps);
List.iter (iter_constr ce) (List.rev newfs);
@@ -449,7 +449,7 @@ let implicits_of_context ctx =
in ExplByPos (i, explname), (true, true, true))
1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
-let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params arity
+let declare_class finite def cum ubinders univs id idbuild paramimpls params arity
template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
let fieldimpls =
(* Make the class implicit in the projections, and the params if applicable. *)
@@ -464,21 +464,21 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
let class_body = it_mkLambda_or_LetIn field params in
let class_type = it_mkProd_or_LetIn arity params in
let class_entry =
- Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
+ Declare.definition_entry ~types:class_type ~univs class_body in
let cst = Declare.declare_constant (snd id)
(DefinitionEntry class_entry, IsDefinition Definition)
in
- let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+ let cstu = (cst, match univs with
+ | Polymorphic_const_entry univs -> Univ.UContext.instance univs
+ | Monomorphic_const_entry _ -> Univ.Instance.empty)
+ in
let inst_type = appvectc (mkConstU cstu)
(Termops.rel_vect 0 (List.length params)) in
let proj_type =
it_mkProd_or_LetIn (mkProd(Name binder_name, inst_type, lift 1 field)) params in
let proj_body =
it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
- let proj_entry =
- Declare.definition_entry ~types:proj_type ~poly
- ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
- in
+ let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
let proj_cst = Declare.declare_constant proj_name
(DefinitionEntry proj_entry, IsDefinition Definition)
in
@@ -495,13 +495,14 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
cref, [Name proj_name, sub, Some proj_cst]
| _ ->
let univs =
- if poly then
+ match univs with
+ | Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
else
- Polymorphic_ind_entry ctx
- else
- Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
+ Polymorphic_ind_entry univs
+ | Monomorphic_const_entry univs ->
+ Monomorphic_ind_entry univs
in
let ind = declare_structure BiFinite ubinders univs (snd id) idbuild paramimpls
params arity template fieldimpls fields
@@ -524,13 +525,15 @@ let declare_class finite def cum poly ubinders ctx id idbuild paramimpls params
params, params
in
let univs, ctx_context, fields =
- if poly then
- let usubst, auctx = Univ.abstract_universes ctx in
+ match univs with
+ | Polymorphic_const_entry univs ->
+ let usubst, auctx = Univ.abstract_universes univs in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
auctx, ctx_context, fields
- else Univ.AUContext.empty, ctx_context, fields
+ | Monomorphic_const_entry _ ->
+ Univ.AUContext.empty, ctx_context, fields
in
let k =
{ cl_univs = univs;
@@ -606,14 +609,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
if isnot_class && List.exists (fun opt -> not (Option.is_empty opt)) priorities then
user_err Pp.(str "Priorities only allowed for type class substructures");
(* Now, younger decl in params and fields is on top *)
- let pl, ctx, arity, template, implpars, params, implfs, fields =
+ let pl, univs, arity, template, implpars, params, implfs, fields =
States.with_state_protection (fun () ->
- typecheck_params_and_fields finite (kind = Class true) idstruc pl s ps notations fs) () in
+ typecheck_params_and_fields finite (kind = Class true) idstruc poly pl s ps notations fs) () in
let sign = structure_signature (fields@params) in
match kind with
| Class def ->
let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
- let gr = declare_class finite def cum poly pl ctx (loc,idstruc) idbuild
+ let gr = declare_class finite def cum pl univs (loc,idstruc) idbuild
implpars params arity template implfs fields is_coe coers priorities sign in
gr
| _ ->
@@ -622,13 +625,14 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
(succ (List.length params)) impls) implfs
in
let univs =
- if poly then
+ match univs with
+ | Polymorphic_const_entry univs ->
if cum then
- Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context ctx)
+ Cumulative_ind_entry (Universes.univ_inf_ind_from_universe_context univs)
else
- Polymorphic_ind_entry ctx
- else
- Monomorphic_ind_entry (Univ.ContextSet.of_context ctx)
+ Polymorphic_ind_entry univs
+ | Monomorphic_const_entry univs ->
+ Monomorphic_ind_entry univs
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-23 19:50:51 +0000