aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml25
-rw-r--r--vernac/comAssumption.ml4
-rw-r--r--vernac/comInductive.ml6
-rw-r--r--vernac/comProgramFixpoint.ml1
-rw-r--r--vernac/lemmas.ml7
-rw-r--r--vernac/obligations.ml7
-rw-r--r--vernac/record.ml36
-rw-r--r--vernac/record.mli1
8 files changed, 37 insertions, 50 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index f4b0015851..b0dba2485a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -146,7 +146,7 @@ let do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imp
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
instance_hook k pri global imps ?hook (ConstRef cst); id
-let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype =
+let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl ids term termtype =
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if program_mode then
let hook _ _ vis gr =
@@ -189,10 +189,10 @@ let declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id
in
ignore (Pfedit.by init_refine)
else if Flags.is_auto_intros () then
- ignore (Pfedit.by (Tacticals.New.tclDO len Tactics.intro));
+ ignore (Pfedit.by (Tactics.auto_intros_tac ids));
(match tac with Some tac -> ignore (Pfedit.by tac) | None -> ())) ()
-let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props len =
+let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
match props with
| Some (true, { CAst.v = CRecord fs }) ->
@@ -275,7 +275,7 @@ let do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~pro
if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
else if program_mode || refine || Option.is_empty term then
- declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl len term termtype
+ declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
id
@@ -341,7 +341,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
do_abstract_instance env sigma ?hook ~global ~poly k u ctx ctx' pri decl imps subst id
else
do_transparent_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
- cty k u ctx ctx' pri decl imps subst id props len
+ cty k u ctx ctx' pri decl imps subst id props
let named_of_rel_context l =
let open Vars in
@@ -370,25 +370,24 @@ let context poly l =
user_err Pp.(str "Anonymous variables not allowed in contexts.")
in
let univs =
- let uctx = Evd.universe_context_set sigma in
match ctx with
| [] -> assert false
- | [_] ->
- if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
- else Monomorphic_const_entry uctx
+ | [_] -> Evd.const_univ_entry ~poly sigma
| _::_::_ ->
+ (** TODO: explain this little belly dance *)
if Lib.sections_are_opened ()
then
begin
+ let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
- if poly then Polymorphic_const_entry Univ.UContext.empty
+ if poly then Polymorphic_const_entry ([||], Univ.UContext.empty)
else Monomorphic_const_entry Univ.ContextSet.empty
end
- else if poly
- then Polymorphic_const_entry (Univ.ContextSet.to_context uctx)
+ else if poly then
+ Evd.const_univ_entry ~poly sigma
else
begin
+ let uctx = Evd.universe_context_set sigma in
Declare.declare_universe_context poly uctx;
Monomorphic_const_entry Univ.ContextSet.empty
end
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index e990f0cd15..8707121306 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -47,7 +47,7 @@ match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
| Monomorphic_const_entry ctx -> ctx
- | Polymorphic_const_entry ctx -> Univ.ContextSet.of_context ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.ContextSet.of_context ctx
in
let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
@@ -79,7 +79,7 @@ match local with
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
let inst = match ctx with
- | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_const_entry _ -> Univ.Instance.empty
in
(gr,inst,Lib.is_modtype_strict ())
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 5ff3032ec4..0c39458a57 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -450,10 +450,10 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
in
let univs =
match uctx with
- | Polymorphic_const_entry uctx ->
+ | Polymorphic_const_entry (nas, uctx) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context uctx)
- else Polymorphic_ind_entry uctx
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context uctx)
+ else Polymorphic_ind_entry (nas, uctx)
| Monomorphic_const_entry uctx ->
Monomorphic_ind_entry uctx
in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3d3d825bd0..d533db7ed9 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -204,7 +204,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
(** FIXME: include locality *)
let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
let gr = ConstRef c in
- let () = UnivNames.register_universe_binders gr (Evd.universe_binders sigma) in
if Impargs.is_implicit_args () || not (List.is_empty impls) then
Impargs.declare_manual_implicits false gr [impls]
in
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 8aa459729c..150f2c6ee9 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -228,7 +228,7 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
| Discharge ->
let impl = false in (* copy values from Vernacentries *)
let univs = match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (_, univs) ->
(* What is going on here? *)
Univ.ContextSet.of_context univs
| Monomorphic_const_entry univs -> univs
@@ -368,10 +368,7 @@ let rec_tac_initializer finite guard thms snl =
| _ -> assert false
let start_proof_with_initialization kind sigma decl recguard thms snl hook =
- let intro_tac (_, (_, (ids, _))) =
- Tacticals.New.tclMAP (function
- | Name id -> Tactics.intro_mustbe_force id
- | Anonymous -> Tactics.intro) (List.rev ids) in
+ let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
let init_tac,guard = match recguard with
| Some (finite,guard,init_tac) ->
let rec_tac = rec_tac_initializer finite guard thms snl in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 97ed43c5f4..c2805674e4 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -667,7 +667,7 @@ let declare_obligation prg obl body ty uctx =
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 ->
+ | 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))
@@ -1004,10 +1004,7 @@ and solve_obligation_by_tac prg obls i tac =
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 uctx = UState.const_univ_entry ~poly:(pi2 prg.prg_kind) ctx in
let prg = {prg with prg_ctx = ctx} in
let def, obl' = declare_obligation prg obl t ty uctx in
obls.(i) <- obl';
diff --git a/vernac/record.ml b/vernac/record.ml
index 7a4c38e972..ac84003266 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -277,12 +277,12 @@ let warn_non_primitive_record =
strbrk" could not be defined as a primitive record")))
(* We build projections *)
-let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers ubinders fieldimpls fields =
+let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields =
let env = Global.env() in
let (mib,mip) = Global.lookup_inductive indsp in
let poly = Declareops.inductive_is_polymorphic mib in
let u = match ctx with
- | Polymorphic_const_entry ctx -> Univ.UContext.instance ctx
+ | Polymorphic_const_entry (_, ctx) -> Univ.UContext.instance ctx
| Monomorphic_const_entry ctx -> Univ.Instance.empty
in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
@@ -324,7 +324,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
(** Already defined by declare_mind silently *)
let kn = Projection.Repr.constant p in
Declare.definition_message fid;
- UnivNames.register_universe_binders (ConstRef kn) ubinders;
kn, mkProj (Projection.make p false,mkRel 1)
else
let ccl = subst_projection fid subst ti in
@@ -360,7 +359,6 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
applist (mkConstU (kn,u),proj_args)
in
Declare.definition_message fid;
- UnivNames.register_universe_binders (ConstRef kn) ubinders;
kn, constr_fip
with Type_errors.TypeError (ctx,te) ->
raise (NotDefinable (BadTypedProj (fid,ctx,te)))
@@ -389,10 +387,10 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
match univs with
| Monomorphic_ind_entry ctx ->
false, Monomorphic_const_entry Univ.ContextSet.empty
- | Polymorphic_ind_entry ctx ->
- true, Polymorphic_const_entry ctx
- | Cumulative_ind_entry cumi ->
- true, Polymorphic_const_entry (Univ.CumulativityInfo.univ_context cumi)
+ | Polymorphic_ind_entry (nas, ctx) ->
+ true, Polymorphic_const_entry (nas, ctx)
+ | Cumulative_ind_entry (nas, cumi) ->
+ true, Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context cumi)
in
let binder_name =
match name with
@@ -443,7 +441,7 @@ let declare_structure finite ubinders univs paramimpls params template ?(kind=St
let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
let rsp = (kn, i) in (* This is ind path of idstruc *)
let cstr = (rsp, 1) in
- let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers ubinders fieldimpls fields in
+ let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
let build = ConstructRef cstr in
let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
let () = Recordops.declare_structure(rsp,cstr,List.rev kinds,List.rev sp_projs) in
@@ -480,7 +478,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
(DefinitionEntry class_entry, IsDefinition Definition)
in
let inst, univs = match univs with
- | Polymorphic_const_entry uctx -> Univ.UContext.instance uctx, univs
+ | Polymorphic_const_entry (_, uctx) -> Univ.UContext.instance uctx, univs
| Monomorphic_const_entry _ -> Univ.Instance.empty, Monomorphic_const_entry Univ.ContextSet.empty
in
let cstu = (cst, inst) in
@@ -496,9 +494,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
in
let cref = ConstRef cst in
Impargs.declare_manual_implicits false cref [paramimpls];
- UnivNames.register_universe_binders cref ubinders;
Impargs.declare_manual_implicits false (ConstRef proj_cst) [List.hd fieldimpls];
- UnivNames.register_universe_binders (ConstRef proj_cst) ubinders;
Classes.set_typeclass_transparency (EvalConstRef cst) false false;
let sub = match List.hd coers with
| Some b -> Some ((if b then Backward else Forward), List.hd priorities)
@@ -508,11 +504,11 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
| _ ->
let univs =
match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (nas, univs) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
else
- Polymorphic_ind_entry univs
+ Polymorphic_ind_entry (nas, univs)
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
@@ -541,8 +537,8 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
in
let univs, ctx_context, fields =
match univs with
- | Polymorphic_const_entry univs ->
- let usubst, auctx = Univ.abstract_universes univs in
+ | Polymorphic_const_entry (nas, univs) ->
+ let usubst, auctx = Univ.abstract_universes nas univs in
let usubst = Univ.make_instance_subst usubst in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
@@ -682,11 +678,11 @@ let definition_structure udecl kind ~template cum poly finite records =
let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
let univs =
match univs with
- | Polymorphic_const_entry univs ->
+ | Polymorphic_const_entry (nas, univs) ->
if cum then
- Cumulative_ind_entry (Univ.CumulativityInfo.from_universe_context univs)
+ Cumulative_ind_entry (nas, Univ.CumulativityInfo.from_universe_context univs)
else
- Polymorphic_ind_entry univs
+ Polymorphic_ind_entry (nas, univs)
| Monomorphic_const_entry univs ->
Monomorphic_ind_entry univs
in
diff --git a/vernac/record.mli b/vernac/record.mli
index 953d5ec3b6..04984030f7 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -20,7 +20,6 @@ val declare_projections :
?kind:Decl_kinds.definition_object_kind ->
Id.t ->
bool list ->
- UnivNames.universe_binders ->
Impargs.manual_implicits list ->
Constr.rel_context ->
(Name.t * bool) list * Constant.t option list
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 17:55:52 +0000