aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--API/API.mli5
-rw-r--r--plugins/funind/indfun.ml1
-rw-r--r--plugins/ltac/rewrite.ml11
-rw-r--r--vernac/classes.ml8
-rw-r--r--vernac/classes.mli1
-rw-r--r--vernac/comDefinition.ml4
-rw-r--r--vernac/comDefinition.mli3
-rw-r--r--vernac/obligations.ml1
-rw-r--r--vernac/vernacentries.ml6
9 files changed, 25 insertions, 15 deletions
diff --git a/API/API.mli b/API/API.mli
index 838613352..ce33e9029 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6052,7 +6052,9 @@ end
module ComDefinition :
sig
- val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
+ val do_definition :
+ program_mode:bool ->
+ Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
end
@@ -6134,6 +6136,7 @@ sig
?abstract:bool ->
?global:bool ->
?refine:bool ->
+ program_mode:bool ->
Decl_kinds.polymorphic ->
Constrexpr.local_binder_expr list ->
Vernacexpr.typeclass_constraint ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 158eb9646..071599d9c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -407,6 +407,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
| [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
ComDefinition.do_definition
+ ~program_mode:false
fname
(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c0060c5a7..7faf8f669 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1781,7 +1781,9 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
- new_instance (Flags.is_universe_polymorphism ())
+ let program_mode = Flags.is_program_mode () in
+ let poly = Flags.is_universe_polymorphism () in
+ new_instance ~program_mode poly
binders instance (Some (true, CAst.make @@ CRecord (fields)))
~global ~generalize:false ~refine:false Hints.empty_hint_info
@@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n =
[cHole; s; m]))
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- ignore(new_instance ~global:glob poly binders instance
- (Some (true, CAst.make @@ CRecord []))
- ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+ let program_mode = Flags.is_program_mode () in
+ ignore(new_instance ~program_mode ~global:glob poly binders instance
+ (Some (true, CAst.make @@ CRecord []))
+ ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
(** Bind to "rewrite" too *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d9c7defa..c2e9a5ab4 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -130,7 +130,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
id
let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
- poly ctx (instid, bk, cl) props ?(generalize=true)
+ ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
let ((loc, instid), pl) = instid in
@@ -215,7 +215,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
Some (Inl fs)
| Some (_, t) -> Some (Inr t)
| None ->
- if Flags.is_program_mode () then Some (Inl [])
+ if program_mode then Some (Inl [])
else None
in
let subst, sigma =
@@ -297,9 +297,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
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 Flags.is_program_mode () || refine || Option.is_empty term then begin
+ else if program_mode || refine || Option.is_empty term then begin
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
- if Flags.is_program_mode () then
+ if program_mode then
let hook vis gr _ =
let cst = match gr with ConstRef kn -> kn | _ -> assert false in
Impargs.declare_manual_implicits false gr ~enriching:false [imps];
diff --git a/vernac/classes.mli b/vernac/classes.mli
index c0f03227c..d47c6a6f8 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -41,6 +41,7 @@ val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
?refine:bool -> (** Allow refinement *)
+ program_mode:bool ->
Decl_kinds.polymorphic ->
local_binder_expr list ->
Vernacexpr.typeclass_constraint ->
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c8b289c9d..883121479 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,11 +104,11 @@ 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 do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
let (ce, evd, univdecl, imps as def) =
interp_definition univdecl bl (pi2 k) red_option c ctypopt
in
- if Flags.is_program_mode () then
+ if program_mode then
let env = Global.env () in
let (c,ctx), sideff = Future.force ce.const_entry_body in
assert(Safe_typing.empty_private_constants = sideff);
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 8dcd31f25..4a65c1e91 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -14,7 +14,8 @@ open Constrexpr
(** {6 Definitions/Let} *)
-val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
+val do_definition : program_mode:bool ->
+ Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
local_binder_expr list -> red_expr option -> constr_expr ->
constr_expr option -> unit Lemmas.declaration_hook -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 181068089..58e4b00fc 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1185,7 +1185,6 @@ let init_program () =
Coqlib.check_required_library ["Coq";"Init";"Specif"];
Coqlib.check_required_library ["Coq";"Program";"Tactics"]
-
let set_program_mode c =
if c then
if !Flags.program_mode then ()
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f6e812168..f5aa15e75 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -478,6 +478,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
| Discharge -> Dumpglob.dump_definition lid true "var"
| Local | Global -> Dumpglob.dump_definition lid false "def"
in
+ let program_mode = Flags.is_program_mode () in
(match def with
| ProveBody (bl,t) -> (* local binders, typ *)
start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
@@ -488,7 +489,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
| Some r ->
let sigma, env = Pfedit.get_current_context () in
Some (snd (Hook.get f_interp_redexp env sigma r)) in
- ComDefinition.do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+ ComDefinition.do_definition ~program_mode id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
let vernac_start_proof ~atts kind l =
let local = enforce_locality_exp atts.locality NoDischarge in
@@ -841,7 +842,8 @@ let vernac_identity_coercion ~atts id qids qidt =
let vernac_instance ~atts abst sup inst props pri =
let global = not (make_section_locality atts.locality) in
Dumpglob.dump_constraint inst false "inst";
- ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri)
+ let program_mode = Flags.is_program_mode () in
+ ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
let vernac_context ~atts l =
if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 11:33:11 +0000