aboutsummaryrefslogtreecommitdiff
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/classes.ml28
-rw-r--r--vernac/classes.mli1
-rw-r--r--vernac/comAssumption.ml26
-rw-r--r--vernac/comAssumption.mli9
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli3
-rw-r--r--vernac/comFixpoint.ml4
-rw-r--r--vernac/declareDef.ml13
-rw-r--r--vernac/declareDef.mli6
-rw-r--r--vernac/obligations.ml10
-rw-r--r--vernac/vernacentries.ml14
-rw-r--r--vernac/vernacextend.ml1
-rw-r--r--vernac/vernacextend.mli1
13 files changed, 45 insertions, 75 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml
index ece9fc8937..5a7f60584a 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration
open Decl_kinds
open Entries
-let refine_instance = ref false
-
-let () = Goptions.(declare_bool_option {
- optdepr = true;
- optname = "definition of instances by refining";
- optkey = ["Refine";"Instance";"Mode"];
- optread = (fun () -> !refine_instance);
- optwrite = (fun b -> refine_instance := b)
-})
-
let set_typeclass_transparency c local b =
Hints.add_hints ~local [typeclasses_db]
(Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b))
@@ -328,6 +318,7 @@ let instance_hook k info global imps ?hook cst =
(match hook with Some h -> h cst | None -> ())
let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
+ (* XXX: Duplication of the declare_constant path *)
let kind = IsDefinition Instance in
let sigma =
let levels = Univ.LSet.union (CVars.universes_of_constr termtype)
@@ -349,14 +340,9 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst
in
let (_, ty_constr) = instance_constructor (k,u) subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- let sigma = Evd.minimize_universes sigma in
- Pretyping.check_evars env (Evd.from_env env) sigma termtype;
- let univs = Evd.check_univ_decl ~poly sigma decl in
- let termtype = to_constr sigma termtype in
+ let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
- (ParameterEntry
- (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
- in
+ (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in
Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma);
instance_hook k pri global imps (ConstRef cst)
@@ -419,7 +405,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
| None ->
pstate) ())
-let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance ~pstate env env' sigma ?hook ~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 }) ->
@@ -503,7 +489,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program
let term = to_constr sigma (Option.get term) in
(declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype;
None)
- else if program_mode || refine || Option.is_empty props then
+ else if program_mode || Option.is_empty props then
declare_instance_open ~pstate 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.") in
id, pstate
@@ -550,7 +536,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl =
sigma, cl, u, c', ctx', ctx, imps, args, decl
-let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode
+let new_instance ~pstate ?(global=false) ~program_mode
poly ctx (instid, bk, cl) props
?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
@@ -566,7 +552,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo
Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode
+ do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
cty k u ctx ctx' pri decl imps subst id props
let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index e7f90ff306..57bb9ce312 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -48,7 +48,6 @@ val declare_instance_constant :
val new_instance :
pstate:Proof_global.t option ->
?global:bool (** Not global by default. *) ->
- ?refine:bool (** Allow refinement *) ->
program_mode:bool ->
Decl_kinds.polymorphic ->
local_binder_expr list ->
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 3406b6276f..635751bb24 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,7 +43,7 @@ let should_axiom_into_instance = function
true
| Global | Local -> !axiom_into_instance
-let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
+let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
match local with
| Discharge when Lib.sections_are_opened () ->
let ctx = match ctx with
@@ -53,11 +53,6 @@ match local with
let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
let _ = declare_variable ident decl in
let () = assumption_message ident in
- let () =
- if not !Flags.quiet && Option.has_some pstate then
- Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++
- strbrk " is not visible from current goals")
- in
let r = VarRef ident in
let () = maybe_declare_manual_implicits true r imps in
let env = Global.env () in
@@ -101,11 +96,11 @@ let next_uctx =
| Polymorphic_entry _ as uctx -> uctx
| Monomorphic_entry _ -> empty_uctx
-let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
let refs, status, _ =
List.fold_left (fun (refs,status,uctx) id ->
let ref',u',status' =
- declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in
+ declare_assumption is_coe k (c,uctx) pl imps false nl id in
(ref',u')::refs, status' && status, next_uctx uctx)
([],true,uctx) idl
in
@@ -137,7 +132,7 @@ let process_assumptions_udecls kind l =
in
udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
-let do_assumptions ~pstate ~program_mode kind nl l =
+let do_assumptions ~program_mode kind nl l =
let open Context.Named.Declaration in
let env = Global.env () in
let udecl, l = process_assumptions_udecls kind l in
@@ -173,12 +168,17 @@ let do_assumptions ~pstate ~program_mode kind nl l =
uvars, (coe,t,imps))
Univ.LSet.empty l
in
+ (* XXX: Using `DeclareDef.prepare_parameter` here directly is not
+ possible as we indeed declare several parameters; however,
+ restrict_universe_context should be called in a centralized place
+ IMO, thus I think we should adapt `prepare_parameter` to handle
+ this case too. *)
let sigma = Evd.restrict_universe_context sigma uvars in
let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
let ubinders = Evd.universe_binders sigma in
pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
let t = replace_vars subst t in
- let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in
+ let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in
let subst' = List.map2
(fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
idl refs
@@ -226,7 +226,7 @@ let named_of_rel_context l =
l ([], [])
in ctx
-let context ~pstate poly l =
+let context poly l =
let env = Global.env() in
let sigma = Evd.from_env env in
let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -291,12 +291,12 @@ let context ~pstate poly l =
let decl = (Discharge, poly, Definitional) in
let nstatus = match b with
| None ->
- pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
+ pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
Declaremods.NoInline (CAst.make id))
| Some b ->
let decl = (Discharge, poly, Definition) in
let entry = Declare.definition_entry ~univs ~types:t b in
- let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
+ let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
Lib.sections_are_opened () || Lib.is_modtype_strict ()
in
status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 7c64317b70..8f37bc0ba4 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -16,8 +16,7 @@ open Decl_kinds
(** {6 Parameters/Assumptions} *)
val do_assumptions
- : pstate:Proof_global.t option
- -> program_mode:bool
+ : program_mode:bool
-> locality * polymorphic * assumption_object_kind
-> Declaremods.inline
-> (ident_decl list * constr_expr) with_coercion list
@@ -26,8 +25,7 @@ val do_assumptions
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
val declare_assumption
- : pstate:Proof_global.t option
- -> coercion_flag
+ : coercion_flag
-> assumption_kind
-> Constr.types Entries.in_universes_entry
-> UnivNames.universe_binders
@@ -42,8 +40,7 @@ val declare_assumption
(** returns [false] if, for lack of section, it declares an assumption
(unless in a module type). *)
val context
- : pstate:Proof_global.t option
- -> Decl_kinds.polymorphic
+ : Decl_kinds.polymorphic
-> local_binder_expr list
-> bool
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d2c986fe5c..4cae4b8a74 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,7 +79,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
check_evars_are_solved ~program_mode env evd;
ce
-let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
let (ce, evd, univdecl, imps as def) =
interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
in
@@ -104,4 +104,4 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct
let ce = check_definition ~program_mode def in
let uctx = Evd.evar_universe_context evd in
let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
- ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps)
+ ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 12853d83e0..fa4860b079 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -17,8 +17,7 @@ open Constrexpr
(** {6 Definitions/Let} *)
val do_definition
- : ontop:Proof_global.t option
- -> program_mode:bool
+ : program_mode:bool
-> ?hook:Lemmas.declaration_hook
-> Id.t
-> definition_kind
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 1912646ffd..00f19f545c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -284,7 +284,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx
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 ~ontop (local, poly, Fixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
fixpoint_message (Some indexes) fixnames;
@@ -319,7 +319,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c
let evd = Evd.restrict_universe_context evd vars in
let ctx = Evd.check_univ_decl ~poly evd pl in
let pl = Evd.universe_binders evd in
- ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx)
+ ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
fixnames fixdecls fixtypes fiximps);
(* Declare the recursive definitions *)
cofixpoint_message fixnames;
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 052832244b..bdda3314ca 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,12 +14,6 @@ open Entries
open Globnames
open Impargs
-let warn_definition_not_visible =
- CWarnings.create ~name:"definition-not-visible" ~category:"implicits"
- Pp.(fun ident ->
- strbrk "Section definition " ++
- Names.Id.print ident ++ strbrk " is not visible from current goals")
-
let warn_local_declaration =
CWarnings.create ~name:"local-declaration" ~category:"scope"
Pp.(fun (id,kind) ->
@@ -33,12 +27,11 @@ let get_locality id ~kind = function
| Local -> true
| Global -> false
-let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ident (local, p, k) ?hook_data ce pl imps =
let fix_exn = Future.fix_exn_of ce.const_entry_body in
let gr = match local with
| Discharge when Lib.sections_are_opened () ->
let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
- let () = if Option.has_some ontop then warn_definition_not_visible ident in
VarRef ident
| Discharge | Local | Global ->
let local = get_locality ident ~kind:"definition" local in
@@ -57,9 +50,9 @@ let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps =
end;
gr
-let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
- declare_definition ~ontop f kind ?hook_data ce pl imps
+ declare_definition f kind ?hook_data ce pl imps
let check_definition_evars ~allow_evars sigma =
let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 8e4f4bf7fb..c4500d0a6b 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -14,8 +14,7 @@ open Decl_kinds
val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool
val declare_definition
- : ontop:Proof_global.t option
- -> Id.t
+ : Id.t
-> definition_kind
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> Safe_typing.private_constants Entries.definition_entry
@@ -24,8 +23,7 @@ val declare_definition
-> GlobRef.t
val declare_fix
- : ontop:Proof_global.t option
- -> ?opaque:bool
+ : ?opaque:bool
-> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
-> definition_kind
-> UnivNames.universe_binders
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index f768278dd7..46c4422d17 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -454,7 +454,7 @@ let obligation_substitution expand prg =
let ints = intset_to (pred (Array.length obls)) in
obl_substitution expand obls ints
-let declare_definition ~ontop prg =
+let declare_definition prg =
let varsubst = obligation_substitution true prg in
let body, typ = subst_prog varsubst prg in
let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None)
@@ -473,7 +473,7 @@ let declare_definition ~ontop prg =
let () = progmap_remove prg in
let ubinders = UState.universe_binders uctx in
let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
- DeclareDef.declare_definition ~ontop prg.prg_name
+ DeclareDef.declare_definition prg.prg_name
prg.prg_kind ce ubinders prg.prg_implicits ?hook_data
let rec lam_index n t acc =
@@ -552,7 +552,7 @@ let declare_mutual_definition l =
(* Declare the recursive definitions *)
let univs = UState.univ_entry ~poly first.prg_ctx in
let fix_exn = Hook.get get_fix_exn () in
- let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs)
+ let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs)
fixnames fixdecls fixtypes fiximps in
(* Declare notations *)
List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
@@ -759,7 +759,7 @@ let update_obls prg obls rem =
else (
match prg'.prg_deps with
| [] ->
- let kn = declare_definition ~ontop:None prg' in
+ let kn = declare_definition prg' in
progmap_remove prg';
Defined kn
| l ->
@@ -1110,7 +1110,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
let obls,_ = prg.prg_obligations in
if Int.equal (Array.length obls) 0 then (
Flags.if_verbose Feedback.msg_info (info ++ str ".");
- let cst = declare_definition ~ontop:None prg in
+ let cst = declare_definition prg in
Defined cst)
else (
let len = Array.length obls in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e1d134f3a9..918852239a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -605,7 +605,7 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def =
| Some r ->
let sigma, env = get_current_or_global_context ~pstate in
Some (snd (Hook.get f_interp_redexp env sigma r)) in
- ComDefinition.do_definition ~ontop:pstate ~program_mode name
+ ComDefinition.do_definition ~program_mode name
(local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook;
pstate
)
@@ -632,7 +632,7 @@ let vernac_exact_proof ~pstate c =
if not status then Feedback.feedback Feedback.AddedAxiom;
pstate
-let vernac_assumption ~atts ~pstate discharge kind l nl =
+let vernac_assumption ~atts discharge kind l nl =
let open DefAttributes in
let local = enforce_locality_exp atts.locality discharge in
let global = local == Global in
@@ -642,7 +642,7 @@ let vernac_assumption ~atts ~pstate discharge kind l nl =
List.iter (fun (lid, _) ->
if global then Dumpglob.dump_definition lid false "ax"
else Dumpglob.dump_definition lid true "var") idl) l;
- let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in
+ let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
if not status then Feedback.feedback Feedback.AddedAxiom
let is_polymorphic_inductive_cumulativity =
@@ -1075,8 +1075,8 @@ let vernac_declare_instance ~atts sup inst pri =
Dumpglob.dump_definition (fst (pi1 inst)) false "inst";
Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
-let vernac_context ~pstate ~poly l =
- if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
+let vernac_context ~poly l =
+ if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
let vernac_existing_instance ~section_local insts =
let glob = not section_local in
@@ -2300,7 +2300,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
unsupported_attributes atts;
vernac_require_open_proof ~pstate (vernac_exact_proof c)
| VernacAssumption ((discharge,kind),nl,l) ->
- with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl;
+ with_def_attributes ~atts vernac_assumption discharge kind l nl;
pstate
| VernacInductive (cum, priv, finite, l) ->
vernac_inductive ~atts cum priv finite l;
@@ -2383,7 +2383,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
with_def_attributes ~atts vernac_declare_instance sup inst info;
pstate
| VernacContext sup ->
- let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in
+ let () = vernac_context ~poly:(only_polymorphism atts) sup in
pstate
| VernacExistingInstance insts ->
with_section_locality ~atts vernac_existing_instance insts;
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index ef06e59316..730f5fd6da 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -36,7 +36,6 @@ type vernac_type =
| VtProofMode of string
(* To be removed *)
| VtMeta
- | VtUnknown
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 4d89eaffd9..54e08d0e95 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -52,7 +52,6 @@ type vernac_type =
| VtProofMode of string
(* To be removed *)
| VtMeta
- | VtUnknown
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
and opacity_guarantee =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 00:35:53 +0000