aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml4
-rw-r--r--plugins/funind/indfun_common.ml18
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml6
-rw-r--r--plugins/ltac/rewrite.ml2
8 files changed, 17 insertions, 23 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 9c1882dc9a..7c0f269481 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -26,7 +26,7 @@ let start_deriving f suchthat lemma =
let env = Global.env () in
let sigma = Evd.from_env env in
- let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
(* create a sort variable for the type of [f] *)
(* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index e38ea992ab..b3a799fb6a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,7 +995,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Ensures by: obvious
i*)
(mk_equation_id f_id)
- (Decl_kinds.Global, false, (Decl_kinds.Proof Decl_kinds.Theorem))
+ Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
evd
lemma_type
in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7b26cb0c74..965ce68811 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -311,7 +311,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
let pstate =
Lemmas.start_proof
new_princ_name
- (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
+ Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
!evd
(EConstr.of_constr new_principle_type)
in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 241da053b7..7070f01c6f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -417,7 +417,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
ComDefinition.do_definition
~program_mode:false
fname
- (Decl_kinds.Global,false,Decl_kinds.Definition) pl
+ Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
bl None body (Some ret_type);
let evd,rev_pconstants =
List.fold_left
@@ -434,7 +434,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
None, evd,List.rev rev_pconstants
| _ ->
- ComFixpoint.do_fixpoint Global false fixpoint_exprl;
+ ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
let evd,rev_pconstants =
List.fold_left
(fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 48cf040919..6d9690096f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -124,26 +124,20 @@ open Declare
let definition_message = Declare.definition_message
-let get_locality = function
-| Discharge -> true
-| Local -> true
-| Global -> false
-
let save id const ?hook uctx (locality,_,kind) =
let fix_exn = Future.fix_exn_of const.const_entry_body in
- let l,r = match locality with
- | Discharge when Lib.sections_are_opened () ->
+ let r = match locality with
+ | Discharge ->
let k = Kindops.logical_kind_of_goal_kind kind in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
- (Local, VarRef id)
- | Discharge | Local | Global ->
- let local = get_locality locality in
+ VarRef id
+ | Global local ->
let k = Kindops.logical_kind_of_goal_kind kind in
let kn = declare_constant id ~local (DefinitionEntry const, k) in
- (locality, ConstRef kn)
+ ConstRef kn
in
- Lemmas.call_hook ?hook ~fix_exn uctx [] l r;
+ Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
definition_message id
let with_full_print f a =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 03568fc6c7..8a16326ba3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let (typ,_) = lemmas_types_infos.(i) in
let pstate = Lemmas.start_proof
lem_id
- (Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
+ Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
!evd
typ in
let pstate = fst @@ Pfedit.by
@@ -866,7 +866,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_complete_id f_id in
let pstate = Lemmas.start_proof lem_id
- (Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
+ Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
(fst lemmas_types_infos.(i)) in
let pstate = fst (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index e2321d233c..5bedb360d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1371,7 +1371,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
in
let pstate = Lemmas.start_proof
na
- (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+ Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
sigma gls_type ~hook:(Lemmas.mk_hook hook) in
let pstate = if Indfun_common.is_strict_tcc ()
then
@@ -1411,7 +1411,7 @@ let com_terminate
hook =
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
let pstate = Lemmas.start_proof thm_name
- (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+ (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
let pstate = fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) pstate in
fst @@ by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
@@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
let evd = Evd.from_ctx uctx in
let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
- let pstate = Lemmas.start_proof eq_name (Global, false, Proof Lemma) ~sign evd
+ let pstate = Lemmas.start_proof eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
let pstate = fst @@ by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index e0a31e7dba..b99e77ab2b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1995,7 +1995,7 @@ let add_morphism_interactive atts m n : Proof_global.t =
let env = Global.env () in
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
- let kind = Decl_kinds.Global, atts.polymorphic,
+ let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:23:08 +0000