aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli7
-rw-r--r--engine/eConstr.ml18
-rw-r--r--engine/eConstr.mli4
-rw-r--r--interp/declare.ml83
-rw-r--r--interp/declare.mli3
-rw-r--r--proofs/pfedit.ml2
-rw-r--r--proofs/pfedit.mli4
-rw-r--r--proofs/proof_global.ml8
-rw-r--r--proofs/proof_global.mli5
-rw-r--r--test-suite/output/UnivBinders.out56
-rw-r--r--test-suite/output/UnivBinders.v49
-rw-r--r--test-suite/prerequisite/bind_univs.v2
-rw-r--r--vernac/classes.ml4
-rw-r--r--vernac/command.ml44
-rw-r--r--vernac/command.mli2
-rw-r--r--vernac/declareDef.ml3
-rw-r--r--vernac/lemmas.ml35
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/record.ml5
19 files changed, 233 insertions, 103 deletions
diff --git a/API/API.mli b/API/API.mli
index 9d1585d60..6227f17c6 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4847,17 +4847,16 @@ sig
set : unit -> unit ;
reset : unit -> unit
}
- type proof_universes = UState.t * Universes.universe_binders option
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
- universes: proof_universes;
+ universes: UState.t;
}
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
- proof_universes
+ UState.t
| Proved of Vernacexpr.opacity_flag *
Vernacexpr.lident option *
proof_object
@@ -5011,7 +5010,7 @@ sig
Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
Proof.t -> Proof.t * bool
val cook_proof :
- unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
+ unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
val get_current_context : unit -> Evd.evar_map * Environ.env
val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index afdceae06..ea098902a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -645,6 +645,24 @@ let eq_constr_universes_proj env sigma m n =
let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
if res then Some !cstrs else None
+let universes_of_constr sigma c =
+ let open Univ in
+ let rec aux s c =
+ match kind sigma c with
+ | Const (_, u) | Ind (_, u) | Construct (_, u) ->
+ LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s
+ | Sort u ->
+ let sort = ESorts.kind sigma u in
+ if Sorts.is_small sort then s
+ else
+ let u = Sorts.univ_of_sort sort in
+ LSet.fold LSet.add (Universe.levels u) s
+ | Evar (k, args) ->
+ let concl = Evd.evar_concl (Evd.find sigma k) in
+ fold sigma aux (aux s (of_constr concl)) c
+ | _ -> fold sigma aux s c
+ in aux LSet.empty c
+
open Context
open Environ
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index e9ef302cf..3e6a13f70 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -201,6 +201,10 @@ val iter_with_binders : Evd.evar_map -> ('a -> 'a) -> ('a -> t -> unit) -> 'a ->
val iter_with_full_binders : Evd.evar_map -> (rel_declaration -> 'a -> 'a) -> ('a -> t -> unit) -> 'a -> t -> unit
val fold : Evd.evar_map -> ('a -> t -> 'a) -> 'a -> t -> 'a
+(** Gather the universes transitively used in the term, including in the
+ type of evars appearing in it. *)
+val universes_of_constr : Evd.evar_map -> t -> Univ.LSet.t
+
(** {6 Substitutions} *)
module Vars :
diff --git a/interp/declare.ml b/interp/declare.ml
index 8fc959b0f..1aeb67afb 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -458,33 +458,61 @@ let declare_universe_context poly ctx =
used to distinguish universes declared in polymorphic sections, which
are discharged and do not remain in scope. *)
-type universe_decl = polymorphic * Nametab.universe_id
+type universe_source =
+ | BoundUniv (* polymorphic universe, bound in a function (this will go away someday) *)
+ | QualifiedUniv of Id.t (* global universe introduced by some global value *)
+ | UnqualifiedUniv (* other global universe *)
-let add_universe p (dp, i) =
+type universe_decl = universe_source * Nametab.universe_id
+
+let add_universe src (dp, i) =
let level = Univ.Level.make dp i in
- let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
- Global.push_context_set p ctx;
- Universes.add_global_universe level p;
- if p then Lib.add_section_context ctx
+ let optpoly = match src with
+ | BoundUniv -> Some true
+ | UnqualifiedUniv -> Some false
+ | QualifiedUniv _ -> None
+ in
+ Option.iter (fun poly ->
+ let ctx = Univ.ContextSet.add_universe level Univ.ContextSet.empty in
+ Global.push_context_set poly ctx;
+ Universes.add_global_universe level poly;
+ if poly then Lib.add_section_context ctx)
+ optpoly
let check_exists sp =
let depth = sections_depth () in
let sp = Libnames.make_path (pop_dirpath_n depth (dirpath sp)) (basename sp) in
- if Nametab.exists_universe sp then alreadydeclared (Id.print (basename sp) ++ str " already exists")
+ if Nametab.exists_universe sp then
+ alreadydeclared (str "Universe " ++ Id.print (basename sp) ++ str " already exists")
else ()
-let cache_universe ((sp, _), (poly, id)) =
+let qualify_univ src (sp,i as orig) =
+ match src with
+ | BoundUniv | UnqualifiedUniv -> orig
+ | QualifiedUniv l ->
+ let sp0, id = Libnames.repr_path sp in
+ let sp0 = DirPath.repr sp0 in
+ Libnames.make_path (DirPath.make (l::sp0)) id, i+1
+
+let cache_universe ((sp, _), (src, id)) =
+ let sp, i = qualify_univ src (sp,1) in
let () = check_exists sp in
- let () = Nametab.push_universe (Nametab.Until 1) sp id in
- add_universe poly id
+ let () = Nametab.push_universe (Nametab.Until i) sp id in
+ add_universe src id
-let load_universe i ((sp, _), (poly, id)) =
+let load_universe i ((sp, _), (src, id)) =
+ let sp, i = qualify_univ src (sp,i) in
let () = Nametab.push_universe (Nametab.Until i) sp id in
- add_universe poly id
+ add_universe src id
-let open_universe i ((sp, _), (poly, id)) =
+let open_universe i ((sp, _), (src, id)) =
+ let sp, i = qualify_univ src (sp,i) in
let () = Nametab.push_universe (Nametab.Exactly i) sp id in
- ()(** add_universe p id Necessary ? *)
+ ()
+
+let discharge_universe = function
+ | _, (BoundUniv, _) -> None
+ | _, ((QualifiedUniv _ | UnqualifiedUniv), _ as x) -> Some x
let input_universe : universe_decl -> Libobject.obj =
declare_object
@@ -492,12 +520,28 @@ let input_universe : universe_decl -> Libobject.obj =
cache_function = cache_universe;
load_function = load_universe;
open_function = open_universe;
- discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
+ discharge_function = discharge_universe;
subst_function = (fun (subst, a) -> (** Actually the name is generated once and for all. *) a);
classify_function = (fun a -> Substitute a) }
-let add_universe poly (id, lev) =
- ignore(Lib.add_leaf id (input_universe (poly, lev)))
+let declare_univ_binders gr pl =
+ if Global.is_polymorphic gr then
+ Universes.register_universe_binders gr pl
+ else
+ let l = match gr with
+ | ConstRef c -> Label.to_id @@ Constant.label c
+ | IndRef (c, _) -> Label.to_id @@ MutInd.label c
+ | VarRef id -> id
+ | ConstructRef _ ->
+ anomaly ~label:"declare_univ_binders"
+ Pp.(str "declare_univ_binders on an constructor reference")
+ in
+ Id.Map.iter (fun id lvl ->
+ match Univ.Level.name lvl with
+ | None -> ()
+ | Some na ->
+ ignore (Lib.add_leaf id (input_universe (QualifiedUniv l, na))))
+ pl
let do_universe poly l =
let in_section = Lib.sections_are_opened () in
@@ -511,7 +555,10 @@ let do_universe poly l =
let lev = Universes.new_univ_id () in
(id, lev)) l
in
- List.iter (add_universe poly) l
+ let src = if poly then BoundUniv else UnqualifiedUniv in
+ List.iter (fun (id,lev) ->
+ ignore(Lib.add_leaf id (input_universe (src, lev))))
+ l
type constraint_decl = polymorphic * Univ.constraints
diff --git a/interp/declare.mli b/interp/declare.mli
index 31883c9d7..f368d164e 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -80,9 +80,8 @@ val recursive_message : bool (** true = fixpoint *) ->
val exists_name : Id.t -> bool
-
-
(** Global universe contexts, names and constraints *)
+val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index c526ae000..31a73db04 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -140,7 +140,7 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
let status = by tac in
let _,(const,univs,_) = cook_proof () in
Proof_global.discard_current ();
- const, status, fst univs
+ const, status, univs
with reraise ->
let reraise = CErrors.push reraise in
Proof_global.discard_current ();
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 2acb678d7..5a317a956 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -35,11 +35,11 @@ val start_proof :
val cook_this_proof :
Proof_global.proof_object ->
(Id.t *
- (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+ (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
val cook_proof : unit ->
(Id.t *
- (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * goal_kind))
+ (Safe_typing.private_constants Entries.definition_entry * UState.t * goal_kind))
(** {6 ... } *)
(** [get_goal_context n] returns the context of the [n]th subgoal of
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c1e1c2eda..535ef2013 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -68,17 +68,16 @@ let _ =
(* Extra info on proofs. *)
type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
- universes: proof_universes;
+ universes: UState.t;
}
type proof_ending =
- | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
+ | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
| Proved of Vernacexpr.opacity_flag *
Vernacexpr.lident option *
proof_object
@@ -333,7 +332,6 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
in
let fpl, univs = Future.split2 fpl in
let universes = if poly || now then Future.force univs else initial_euctx 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
normalise them for the kernel. *)
@@ -409,7 +407,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
in
let entries = Future.map2 entry_fn fpl initial_goals in
{ id = pid; entries = entries; persistence = strength;
- universes = (universes, binders) },
+ universes },
fun pr_ending -> CEphemeron.get terminator pr_ending
let return_proof ?(allow_partial=false) () =
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 059459042..27e99f218 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -37,18 +37,17 @@ val compact_the_proof : unit -> unit
(i.e. an proof ending command) and registers the appropriate
values. *)
type lemma_possible_guards = int list list
-type proof_universes = UState.t * Universes.universe_binders option
type proof_object = {
id : Names.Id.t;
entries : Safe_typing.private_constants Entries.definition_entry list;
persistence : Decl_kinds.goal_kind;
- universes: proof_universes;
+ universes: UState.t;
}
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
- proof_universes
+ UState.t
| Proved of Vernacexpr.opacity_flag *
Vernacexpr.lident option *
proof_object
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index f69379a57..d6d410d1a 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -44,26 +44,45 @@ bar@{u} = nat
bar is universe polymorphic
foo@{u Top.17 v} =
Type@{Top.17} -> Type@{v} -> Type@{u}
- : Type@{max(u+1, Top.17+1, v+1)}
+ : Type@{max(u+1,Top.17+1,v+1)}
(* u Top.17 v |= *)
foo is universe polymorphic
-Monomorphic mono = Type@{u}
- : Type@{u+1}
-(* {u} |= *)
+Monomorphic mono = Type@{mono.u}
+ : Type@{mono.u+1}
+(* {mono.u} |= *)
mono is not universe polymorphic
+mono
+ : Type@{mono.u+1}
+Type@{mono.u}
+ : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+monomono
+ : Type@{MONOU+1}
+mono.monomono
+ : Type@{mono.MONOU+1}
+monomono
+ : Type@{MONOU+1}
+mono
+ : Type@{mono.u+1}
+The command has indeed failed with message:
+Universe u already exists.
+bobmorane =
+let tt := Type@{tt.v} in let ff := Type@{ff.v} in tt -> ff
+ : Type@{max(tt.u,ff.u)}
The command has indeed failed with message:
Universe u already bound.
foo@{E M N} =
Type@{M} -> Type@{N} -> Type@{E}
- : Type@{max(E+1, M+1, N+1)}
+ : Type@{max(E+1,M+1,N+1)}
(* E M N |= *)
foo is universe polymorphic
foo@{Top.16 Top.17 Top.18} =
Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16}
- : Type@{max(Top.16+1, Top.17+1, Top.18+1)}
+ : Type@{max(Top.16+1,Top.17+1,Top.18+1)}
(* Top.16 Top.17 Top.18 |= *)
foo is universe polymorphic
@@ -88,9 +107,10 @@ The command has indeed failed with message:
This object does not support universe names.
The command has indeed failed with message:
Cannot enforce v < u because u < gU < gV < v
-Monomorphic bind_univs.mono = Type@{u}
- : Type@{u+1}
-(* {u} |= *)
+Monomorphic bind_univs.mono =
+Type@{bind_univs.mono.u}
+ : Type@{bind_univs.mono.u+1}
+(* {bind_univs.mono.u} |= *)
bind_univs.mono is not universe polymorphic
bind_univs.poly@{u} = Type@{u}
@@ -99,12 +119,12 @@ bind_univs.poly@{u} = Type@{u}
bind_univs.poly is universe polymorphic
insec@{v} = Type@{u} -> Type@{v}
- : Type@{max(u+1, v+1)}
+ : Type@{max(u+1,v+1)}
(* v |= *)
insec is universe polymorphic
insec@{u v} = Type@{u} -> Type@{v}
- : Type@{max(u+1, v+1)}
+ : Type@{max(u+1,v+1)}
(* u v |= *)
insec is universe polymorphic
@@ -125,28 +145,28 @@ inmod@{u} = Type@{u}
inmod is universe polymorphic
Applied.infunct@{u v} =
inmod@{u} -> Type@{v}
- : Type@{max(u+1, v+1)}
+ : Type@{max(u+1,v+1)}
(* u v |= *)
Applied.infunct is universe polymorphic
-axfoo@{i Top.33 Top.34} : Type@{Top.33} -> Type@{i}
-(* i Top.33 Top.34 |= *)
+axfoo@{i Top.41 Top.42} : Type@{Top.41} -> Type@{i}
+(* i Top.41 Top.42 |= *)
axfoo is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo
-axbar@{i Top.33 Top.34} : Type@{Top.34} -> Type@{i}
-(* i Top.33 Top.34 |= *)
+axbar@{i Top.41 Top.42} : Type@{Top.42} -> Type@{i}
+(* i Top.41 Top.42 |= *)
axbar is universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axbar
-axfoo' : Type@{Top.36} -> Type@{i}
+axfoo' : Type@{Top.44} -> Type@{axbar'.i}
axfoo' is not universe polymorphic
Argument scope is [type_scope]
Expands to: Constant Top.axfoo'
-axbar' : Type@{Top.36} -> Type@{i}
+axbar' : Type@{Top.44} -> Type@{axbar'.i}
axbar' is not universe polymorphic
Argument scope is [type_scope]
diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v
index 116d5e5e9..266d94ad9 100644
--- a/test-suite/output/UnivBinders.v
+++ b/test-suite/output/UnivBinders.v
@@ -1,6 +1,6 @@
Set Universe Polymorphism.
Set Printing Universes.
-Unset Strict Universe Declaration.
+(* Unset Strict Universe Declaration. *)
(* universe binders on inductive types and record projections *)
Inductive Empty@{u} : Type@{u} := .
@@ -25,14 +25,59 @@ Print wrap.
Instance bar@{u} : Wrap@{u} Set. Proof. exact nat. Qed.
Print bar.
+Unset Strict Universe Declaration.
(* The universes in the binder come first, then the extra universes in
order of appearance. *)
Definition foo@{u +} := Type -> Type@{v} -> Type@{u}.
Print foo.
+Set Strict Universe Declaration.
(* Binders even work with monomorphic definitions! *)
Monomorphic Definition mono@{u} := Type@{u}.
Print mono.
+Check mono.
+Check Type@{mono.u}.
+
+Module mono.
+ Fail Monomorphic Universe u.
+ Monomorphic Universe MONOU.
+
+ Monomorphic Definition monomono := Type@{MONOU}.
+ Check monomono.
+End mono.
+Check mono.monomono. (* qualified MONOU *)
+Import mono.
+Check monomono. (* unqualified MONOU *)
+Check mono. (* still qualified mono.u *)
+
+Monomorphic Constraint Set < Top.mono.u.
+
+Module mono2.
+ Monomorphic Universe u.
+End mono2.
+
+Fail Monomorphic Definition mono2@{u} := Type@{u}.
+
+Module SecLet.
+ Unset Universe Polymorphism.
+ Section foo.
+ (* Fail Let foo@{} := Type@{u}. (* doesn't parse: Let foo@{...} doesn't exist *) *)
+ Unset Strict Universe Declaration.
+ Let tt : Type@{u} := Type@{v}. (* names disappear in the ether *)
+ Let ff : Type@{u}. Proof. exact Type@{v}. Qed. (* if Set Universe Polymorphism: universes are named ff.u and ff.v. Otherwise names disappear into space *)
+ Definition bobmorane := tt -> ff.
+ End foo.
+ Print bobmorane. (*
+ bobmorane@{Top.15 Top.16 ff.u ff.v} =
+ let tt := Type@{Top.16} in let ff := Type@{ff.v} in tt -> ff
+ : Type@{max(Top.15,ff.u)}
+ (* Top.15 Top.16 ff.u ff.v |= Top.16 < Top.15
+ ff.v < ff.u
+ *)
+
+ bobmorane is universe polymorphic
+ *)
+End SecLet.
(* fun x x => foo is nonsense with local binders *)
Fail Definition fo@{u u} := Type@{u}.
@@ -61,7 +106,7 @@ Monomorphic Universes gU gV. Monomorphic Constraint gU < gV.
Fail Lemma foo@{u v|u < gU, gV < v, v < u} : nat.
(* Universe binders survive through compilation, sections and modules. *)
-Require bind_univs.
+Require TestSuite.bind_univs.
Print bind_univs.mono.
Print bind_univs.poly.
diff --git a/test-suite/prerequisite/bind_univs.v b/test-suite/prerequisite/bind_univs.v
index f17c00e9d..e834fde11 100644
--- a/test-suite/prerequisite/bind_univs.v
+++ b/test-suite/prerequisite/bind_univs.v
@@ -3,3 +3,5 @@
Monomorphic Definition mono@{u} := Type@{u}.
Polymorphic Definition poly@{u} := Type@{u}.
+
+Monomorphic Universe reqU.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index b80741269..cb1d2f7c7 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -126,7 +126,7 @@ let declare_instance_constant k info global imps ?hook id decl poly evm term ter
let cdecl = (DefinitionEntry entry, kind) in
let kn = Declare.declare_constant id cdecl in
Declare.definition_message id;
- Universes.register_universe_binders (ConstRef kn) (Evd.universe_binders evm);
+ Declare.declare_univ_binders (ConstRef kn) (Evd.universe_binders evm);
instance_hook k info global imps ?hook (ConstRef kn);
id
@@ -208,7 +208,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(ParameterEntry
(None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- Universes.register_universe_binders (ConstRef cst) (Evd.universe_binders !evars);
+ Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders !evars);
instance_hook k pri global imps ?hook (ConstRef cst); id
end
else (
diff --git a/vernac/command.ml b/vernac/command.ml
index 01c7f149b..66d4fe984 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -95,7 +95,7 @@ let interp_definition pl bl poly red_option c ctypopt =
let impls, ((env_bl, ctx), imps1) = interp_context_evars env evdref bl in
let ctx = List.map (fun d -> map_rel_decl EConstr.Unsafe.to_constr d) ctx in
let nb_args = Context.Rel.nhyps ctx in
- let imps,pl,ce =
+ let imps,ce =
match ctypopt with
None ->
let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -105,11 +105,10 @@ let interp_definition pl bl poly 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 ~poly evd decl in
- let binders = Evd.universe_binders evd in
- imps1@(Impargs.lift_implicits nb_args imps2), binders,
+ let vars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args imps2),
definition_entry ~univs:uctx body
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
@@ -131,23 +130,22 @@ let interp_definition pl bl poly red_option c ctypopt =
in
if not (try List.for_all chk imps2 with Not_found -> false)
then warn_implicits_in_term ();
- 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 ~poly ctx decl in
- let binders = Evd.universe_binders evd in
- imps1@(Impargs.lift_implicits nb_args impsty), binders,
- definition_entry ~types:typ
- ~univs:uctx body
+ let bodyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr body) in
+ let tyvars = EConstr.universes_of_constr !evdref (EConstr.of_constr ty) in
+ let vars = Univ.LSet.union bodyvars tyvars in
+ let () = evdref := Evd.restrict_universe_context !evdref vars in
+ let uctx = Evd.check_univ_decl ~poly !evdref decl in
+ imps1@(Impargs.lift_implicits nb_args impsty),
+ definition_entry ~types:typ ~univs:uctx body
in
- red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, pl, imps
+ (red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, decl, imps)
-let check_definition (ce, evd, _, _, imps) =
+let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd Evd.empty;
ce
let do_definition ident k univdecl bl red_option c ctypopt hook =
- let (ce, evd, univdecl, pl', imps as def) =
+ let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
if Flags.is_program_mode () then
@@ -168,7 +166,7 @@ let do_definition ident k univdecl bl red_option c ctypopt hook =
ignore(Obligations.add_definition
ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ~hook obls)
else let ce = check_definition def in
- ignore(DeclareDef.declare_definition ident k ce pl' imps
+ ignore(DeclareDef.declare_definition ident k ce (Evd.universe_binders evd) imps
(Lemmas.mk_hook
(fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
@@ -224,7 +222,7 @@ match local with
let kn = declare_constant ident ~local decl in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = assumption_message ident in
let () = if do_instance then Typeclasses.declare_instance None false gr in
let () = if is_coe then Class.try_add_new_coercion gr ~local p in
@@ -712,7 +710,7 @@ let declare_mutual_inductive_with_eliminations mie pl impls =
let ind = (mind,i) in
let gr = IndRef ind in
maybe_declare_manual_implicits false gr indimpls;
- Universes.register_universe_binders gr pl;
+ Declare.declare_univ_binders gr pl;
List.iteri
(fun j impls ->
maybe_declare_manual_implicits false
@@ -1268,7 +1266,7 @@ let collect_evars_of_term evd c ty =
Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
evars (Evd.from_ctx (Evd.evar_universe_context evd))
-let do_program_recursive local p fixkind fixl ntns =
+let do_program_recursive local poly fixkind fixl ntns =
let isfix = fixkind != Obligations.IsCoFixpoint in
let (env, rec_sign, pl, evd), fix, info =
interp_recursive isfix fixl ntns
@@ -1310,8 +1308,8 @@ let do_program_recursive local p fixkind fixl ntns =
end in
let ctx = Evd.evar_universe_context evd in
let kind = match fixkind with
- | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
- | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+ | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
+ | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
in
Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
diff --git a/vernac/command.mli b/vernac/command.mli
index 070f3e112..a1f916c78 100644
--- a/vernac/command.mli
+++ b/vernac/command.mli
@@ -28,7 +28,7 @@ val do_constraint : polymorphic ->
val interp_definition :
Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
- Univdecls.universe_decl * Universes.universe_binders * Impargs.manual_implicits
+ Univdecls.universe_decl * Impargs.manual_implicits
val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 980db4109..dfac78c04 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,7 +36,7 @@ let declare_global_definition ident ce local k pl imps =
let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
let gr = ConstRef kn in
let () = maybe_declare_manual_implicits false gr imps in
- let () = Universes.register_universe_binders gr pl in
+ let () = Declare.declare_univ_binders gr pl in
let () = definition_message ident in
gr
@@ -49,6 +49,7 @@ let declare_definition ident (local, p, k) ce pl imps hook =
let () = definition_message ident in
let gr = VarRef ident in
let () = maybe_declare_manual_implicits false gr imps in
+ let () = Declare.declare_univ_binders gr pl in
let () = if Proof_global.there_are_pending_proofs () then
warn_definition_not_visible ident
in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 42631a15b..200c2260e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -177,7 +177,7 @@ let look_for_possibly_mutual_statements = function
(* Saving a goal *)
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const uctx do_guard (locality,poly,kind) hook =
let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
try
let const = adjust_guardness_conditions const do_guard in
@@ -204,7 +204,7 @@ let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
(locality, ConstRef kn)
in
definition_message id;
- Universes.register_universe_binders r (Option.default Universes.empty_binders pl);
+ Declare.declare_univ_binders r (UState.universe_binders uctx);
call_hook (fun exn -> exn) hook l r
with e when CErrors.noncritical e ->
let e = CErrors.push e in
@@ -286,17 +286,17 @@ let save_hook = ref ignore
let set_save_hook f = save_hook := f
let save_named ?export_seff proof =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
- save ?export_seff id const cstrs pl do_guard persistence hook
+ let id,const,uctx,do_guard,persistence,hook = proof in
+ save ?export_seff id const uctx do_guard persistence hook
let check_anonymity id save_ident =
if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
user_err Pp.(str "This command can only be used for unnamed theorem.")
let save_anonymous ?export_seff proof save_ident =
- let id,const,(cstrs,pl),do_guard,persistence,hook = proof in
+ let id,const,uctx,do_guard,persistence,hook = proof in
check_anonymity id save_ident;
- save ?export_seff save_ident const cstrs pl do_guard persistence hook
+ save ?export_seff save_ident const uctx do_guard persistence hook
(* Admitted *)
@@ -312,7 +312,7 @@ let admit (id,k,e) pl hook () =
| Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
in
let () = assumption_message id in
- Universes.register_universe_binders (ConstRef kn) (Option.default Universes.empty_binders pl);
+ Declare.declare_univ_binders (ConstRef kn) pl;
call_hook (fun exn -> exn) hook Global (ConstRef kn)
(* Starting a goal *)
@@ -330,8 +330,8 @@ let get_proof proof do_guard hook opacity =
let universe_proof_terminator compute_guard hook =
let open Proof_global in
make_terminator begin function
- | Admitted (id,k,pe,(ctx,pl)) ->
- admit (id,k,pe) pl (hook (Some ctx)) ();
+ | Admitted (id,k,pe,ctx) ->
+ admit (id,k,pe) (UState.universe_binders ctx) (hook (Some ctx)) ();
Feedback.feedback Feedback.AddedAxiom
| Proved (opaque,idopt,proof) ->
let is_opaque, export_seff = match opaque with
@@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook =
| Vernacexpr.Opaque -> true, false
in
let proof = get_proof proof compute_guard
- (hook (Some (fst proof.Proof_global.universes))) is_opaque in
+ (hook (Some (proof.Proof_global.universes))) is_opaque in
begin match idopt with
| None -> save_named ~export_seff proof
| Some (_,id) -> save_anonymous ~export_seff proof id
@@ -417,7 +417,7 @@ let start_proof_with_initialization kind ctx decl recguard thms snl hook =
| (id,(t,(_,imps)))::other_thms ->
let hook ctx strength ref =
let ctx = match ctx with
- | None -> Evd.empty_evar_universe_context
+ | None -> UState.empty
| Some ctx -> ctx
in
let other_thms_data =
@@ -426,9 +426,9 @@ 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 ~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 uctx = UState.check_univ_decl ~poly:(pi2 kind) ctx decl in
+ List.map_i (save_remaining_recthms kind norm uctx body opaq) 1 other_thms in
let thms_data = (strength,ref,imps)::other_thms_data in
List.iter (fun (strength,ref,imps) ->
maybe_declare_manual_implicits false ref imps;
@@ -496,7 +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 = UState.const_univ_entry ~poly:(pi2 k) (fst universes) in
+ let ctx = UState.const_univ_entry ~poly:(pi2 k) 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 ->
@@ -518,12 +518,9 @@ let save_proof ?proof = function
Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
| _ -> None in
let decl = Proof_global.get_universe_decl () in
- let evd = Evd.from_ctx universes in
let poly = pi2 k 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))
+ let ctx = UState.check_univ_decl ~poly universes decl in
+ Admitted(id,k,(sec_vars, (typ, ctx), None), universes)
in
Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
| Vernacexpr.Proved (is_opaque,idopt) ->
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 1046d68f8..24d664951 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -833,7 +833,7 @@ let obligation_terminator name num guard hook auto pf =
let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in
let ty = entry.Entries.const_entry_type in
let (body, cstr), () = Future.force entry.Entries.const_entry_body in
- let sigma = Evd.from_ctx (fst uctx) in
+ let sigma = Evd.from_ctx uctx in
let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
Inductiveops.control_only_guard (Global.env ()) body;
(** Declare the obligation ourselves and drop the hook *)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1d255b08e..1cdc538b5 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -613,7 +613,7 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
States.with_state_protection (fun () ->
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
+ let gr = 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 pl univs (loc,idstruc) idbuild
@@ -638,3 +638,6 @@ let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cf
idbuild implpars params arity template implfs
fields is_coe (List.map (fun coe -> not (Option.is_empty coe)) coers) sign in
IndRef ind
+ in
+ Declare.declare_univ_binders gr pl;
+ gr
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 06:29:23 +0000