aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml6
-rw-r--r--plugins/funind/indfun_common.ml2
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/ltac/rewrite.ml5
7 files changed, 23 insertions, 15 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 22e20e2c52..8c2cf3c553 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -19,7 +19,8 @@ let start_deriving f suchthat name : Lemmas.t =
let env = Global.env () in
let sigma = Evd.from_env env in
- let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
+ let poly = false in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior,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
@@ -40,7 +41,7 @@ let start_deriving f suchthat name : Lemmas.t =
in
let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) () in
- let lemma = Lemmas.start_dependent_lemma ~name ~kind ~info goals in
+ let lemma = Lemmas.start_dependent_lemma ~name ~poly ~kind ~info goals in
Lemmas.pf_map (Proof_global.map_proof begin fun p ->
Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
end) lemma
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 9c593a55d8..c37e6f7402 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -995,8 +995,8 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
Ensures by: obvious
i*)
~name:(mk_equation_id f_id)
- ~kind:Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-
+ ~poly:false
+ ~kind:(Decl_kinds.(Global ImportDefaultBehavior, Proof Theorem))
evd
lemma_type
in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 1154198d43..1b447bd26a 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -308,8 +308,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
evd := sigma;
let hook = DeclareDef.Hook.make (hook new_principle_type) in
let lemma =
- Lemmas.start_lemma ~name:new_princ_name
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+ Lemmas.start_lemma
+ ~name:new_princ_name
+ ~poly:false
+ ~kind:(Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem))
!evd
(EConstr.of_constr new_principle_type)
in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17c79e0e6c..a5a07934ac 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -123,7 +123,7 @@ open Declare
let definition_message = Declare.definition_message
-let save id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx (locality,kind) =
let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
let r = match locality with
| Discharge ->
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 48b5e56635..e5b0a5d032 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -805,7 +805,8 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let (typ,_) = lemmas_types_infos.(i) in
let lemma = Lemmas.start_lemma
~name:lem_id
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+ ~poly:false
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem)
!evd
typ in
let lemma = fst @@ Lemmas.by
@@ -866,8 +867,9 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_complete_id f_id in
let lemma = Lemmas.start_lemma ~name:lem_id
- ~kind:Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
- (fst lemmas_types_infos.(i)) in
+ ~poly:false
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior,Proof Theorem) sigma
+ (fst lemmas_types_infos.(i)) in
let lemma = fst (Lemmas.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i))) lemma) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c97b39ff79..187d907dc5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1370,7 +1370,8 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook) () in
let lemma = Lemmas.start_lemma
~name:na
- ~kind:Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~info
+ ~poly:false (* FIXME *)
+ ~kind:Decl_kinds.(Global ImportDefaultBehavior, Proof Lemma) ~info
sigma gls_type in
let lemma = if Indfun_common.is_strict_tcc ()
then
@@ -1411,7 +1412,8 @@ let com_terminate
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
let info = Lemmas.Info.make ~hook () in
let lemma = Lemmas.start_lemma ~name:thm_name
- ~kind:(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
+ ~poly:false (*FIXME*)
+ ~kind:(Global ImportDefaultBehavior, Proof Lemma)
~sign:(Environ.named_context_val env)
~info
ctx
@@ -1460,7 +1462,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 lemma = Lemmas.start_lemma ~name:eq_name ~kind:(Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+ let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~kind:(Global ImportDefaultBehavior, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 49265802ae..d87b7a1770 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1994,7 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.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 Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
+ let poly = atts.polymorphic in
+ let kind = Decl_kinds.(Global ImportDefaultBehavior),
Decl_kinds.DefinitionBody Decl_kinds.Instance
in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -2010,7 +2011,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let info = Lemmas.Info.make ~hook () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~name:instance_id ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~kind ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:54:00 +0000