aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml81
-rw-r--r--plugins/funind/functional_principles_proofs.ml13
-rw-r--r--plugins/funind/functional_principles_types.ml40
-rw-r--r--plugins/funind/functional_principles_types.mli2
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/indfun.ml8
-rw-r--r--plugins/funind/indfun_common.ml11
-rw-r--r--plugins/funind/indfun_common.mli7
-rw-r--r--plugins/funind/invfun.ml26
-rw-r--r--plugins/funind/invfun.mli2
-rw-r--r--plugins/funind/recdef.ml24
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/rewrite.ml20
-rw-r--r--plugins/setoid_ring/newring.ml2
15 files changed, 101 insertions, 141 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index a884ab3cf6..e34150f2b3 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -8,16 +8,9 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Constr
open Context
open Context.Named.Declaration
-let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body)
- : Evd.side_effects Entries.const_entry_body =
- Future.chain x begin fun ((b,ctx),fx) ->
- (f b , ctx) , fx
- end
-
(** [start_deriving f suchthat lemma] starts a proof of [suchthat]
(which can contain references to [f]) in the context extended by
[f:=?x]. When the proof ends, [f] is defined as the value of [?x]
@@ -26,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.(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
@@ -36,71 +30,18 @@ let start_deriving f suchthat name : Lemmas.t =
(* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
let goals =
let open Proofview in
- TCons ( env , sigma , f_type_type , (fun sigma f_type ->
+ TCons ( env , sigma , f_type_type , (fun sigma f_type ->
TCons ( env , sigma , f_type , (fun sigma ef ->
- let f_type = EConstr.Unsafe.to_constr f_type in
- let ef = EConstr.Unsafe.to_constr ef in
- let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
- let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
- TCons ( env' , sigma , suchthat , (fun sigma _ ->
- TNil sigma))))))
- in
-
- (* The terminator handles the registering of constants when the proof is closed. *)
- let terminator com =
- (* Extracts the relevant information from the proof. [Admitted]
- and [Save] result in user errors. [opaque] is [true] if the
- proof was concluded by [Qed], and [false] if [Defined]. [f_def]
- and [lemma_def] correspond to the proof of [f] and of
- [suchthat], respectively. *)
- let (opaque,f_def,lemma_def) =
- match com with
- | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
- | Lemmas.Proved (_,Some _,_) ->
- CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
- | Lemmas.Proved (opaque, None, obj) ->
- match Proof_global.(obj.entries) with
- | [_;f_def;lemma_def] ->
- opaque <> Proof_global.Transparent , f_def , lemma_def
- | _ -> assert false
- in
- (* The opacity of [f_def] is adjusted to be [false], as it
- must. Then [f] is declared in the global environment. *)
- let f_def = { f_def with Entries.const_entry_opaque = false } in
- let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
- let f_kn = Declare.declare_constant f f_def in
- let f_kn_term = mkConst f_kn in
- (* In the type and body of the proof of [suchthat] there can be
- references to the variable [f]. It needs to be replaced by
- references to the constant [f] declared above. This substitution
- performs this precise action. *)
- let substf c = Vars.replace_vars [f,f_kn_term] c in
- (* Extracts the type of the proof of [suchthat]. *)
- let lemma_pretype =
- match Entries.(lemma_def.const_entry_type) with
- | Some t -> t
- | None -> assert false (* Proof_global always sets type here. *)
- in
- (* The references of [f] are subsituted appropriately. *)
- let lemma_type = substf lemma_pretype in
- (* The same is done in the body of the proof. *)
- let lemma_body =
- map_const_entry_body substf Entries.(lemma_def.const_entry_body)
- in
- let lemma_def = let open Entries in { lemma_def with
- const_entry_body = lemma_body ;
- const_entry_type = Some lemma_type ;
- const_entry_opaque = opaque ; }
- in
- let lemma_def =
- Entries.DefinitionEntry lemma_def ,
- Decl_kinds.(IsProof Proposition)
- in
- ignore (Declare.declare_constant name lemma_def)
+ let f_type = EConstr.Unsafe.to_constr f_type in
+ let ef = EConstr.Unsafe.to_constr ef in
+ let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
+ let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
+ TCons ( env' , sigma , suchthat , (fun sigma _ ->
+ TNil sigma))))))
in
- let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
- let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
+ let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
+ let lemma = Lemmas.start_dependent_lemma ~name ~poly ~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 ce3b5a82d6..a904b81d81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,14 +990,19 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
]
in
(* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
+ let info = Lemmas.Info.make
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+
let lemma = Lemmas.start_lemma
(*i The next call to mk_equation_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
- (mk_equation_id f_id)
- Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
- evd
- lemma_type
+ ~name:(mk_equation_id f_id)
+ ~poly:false
+ ~info
+ evd
+ lemma_type
in
let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2fe1d1ff40..edda2f2eef 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -19,7 +19,6 @@ open Vars
open Namegen
open Names
open Pp
-open Entries
open Tactics
open Context.Rel.Declaration
open Indfun_common
@@ -307,11 +306,11 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
in
let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
evd := sigma;
- let hook = Lemmas.mk_hook (hook new_principle_type) in
+ let hook = DeclareDef.Hook.make (hook new_principle_type) in
let lemma =
Lemmas.start_lemma
- new_princ_name
- Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+ ~name:new_princ_name
+ ~poly:false
!evd
(EConstr.of_constr new_principle_type)
in
@@ -325,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* end; *)
let open Proof_global in
- let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
match entries with
| [entry] ->
- (id,(entry,persistence)), hook
+ name, entry, hook
| _ ->
CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
@@ -371,7 +370,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
ignore(
Declare.declare_constant
name
- (DefinitionEntry ce,
+ (Declare.DefinitionEntry ce,
Decl_kinds.IsDefinition (Decl_kinds.Scheme))
);
Declare.definition_message name;
@@ -380,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort InProp;
register_with_sort InSet
in
- let ((id,(entry,g_kind)),hook) =
+ let id,entry,hook =
build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
proof_tac hook
in
@@ -388,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
- save new_princ_name entry ~hook uctx g_kind
+ save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
with e when CErrors.noncritical e ->
raise (Defining_principle e)
@@ -471,7 +470,7 @@ let get_funs_constant mp =
exception No_graph_found
exception Found_type of int
-let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects definition_entry list =
+let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Proof_global.proof_entry list =
let env = Global.env () in
let funs = List.map fst fas in
let first_fun = List.hd funs in
@@ -519,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
s::l_schemes -> s,l_schemes
| _ -> anomaly (Pp.str "")
in
- let ((_,(const,_)),_) =
+ let _,const,_ =
try
build_functional_principle evd false
first_type
@@ -541,7 +540,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
with Option.IsNone -> (* non recursive definition *)
false
in
- let const = {const with const_entry_opaque = opacity } in
+ let const = {const with Proof_global.proof_entry_opaque = opacity } in
(* The others are just deduced *)
if List.is_empty other_princ_types
then
@@ -552,7 +551,8 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
let sorts = Array.of_list sorts in
List.map (compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = const.const_entry_body, const.const_entry_type in
+ let open Proof_global in
+ let first_princ_body,first_princ_type = const.proof_entry_body, const.proof_entry_type in
let ctxt,fix = decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = destFix fix in
let other_result =
@@ -576,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
)
ta;
- (* If we reach this point, the two principle are not mutually recursive
- We fall back to the previous method
- *)
- let ((_,(const,_)),_) =
+ (* If we reach this point, the two principle are not mutually recursive
+ We fall back to the previous method
+ *)
+ let _,const,_ =
build_functional_principle
evd
false
@@ -596,9 +596,9 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects def
Termops.it_mkLambda_or_LetIn (mkFix((idxs,i),decl)) ctxt
in
{const with
- const_entry_body =
+ proof_entry_body =
(Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
- const_entry_type = Some scheme_type
+ proof_entry_type = Some scheme_type
}
)
other_fun_princ_types
@@ -638,7 +638,7 @@ let build_scheme fas =
ignore
(Declare.declare_constant
princ_id
- (DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
Declare.definition_message princ_id
)
fas
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index 3f70e870ab..b4f6f92f9c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -34,7 +34,7 @@ val generate_functional_principle :
exception No_graph_found
val make_scheme : Evd.evar_map ref ->
- (pconstant*Sorts.family) list -> Evd.side_effects Entries.definition_entry list
+ (pconstant*Sorts.family) list -> Evd.side_effects Proof_global.proof_entry list
val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit
val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ef9d91c7fa..e20d010c71 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl =
let classify_as_Fixpoint recsl =
Vernac_classifier.classify_vernac
- (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+ (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
let classify_funind recsl =
match classify_as_Fixpoint recsl with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 201d953692..bb4e745fe9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1506,7 +1506,7 @@ let do_build_inductive
let _time2 = System.get_time () in
try
with_full_print
- (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+ (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters))
Declarations.Finite
with
| UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..d305a58ccc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
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 ImportDefaultBehavior,false,Definition) pl
+ ~name:fname
+ ~poly:false
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~kind:Decl_kinds.Definition pl
bl None body (Some ret_type);
let evd,rev_pconstants =
List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
in
None, evd,List.rev rev_pconstants
| _ ->
- ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+ ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly: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 7683ce1757..254760cb50 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,14 +118,13 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
(* Copy of the standard save mechanism but without the much too *)
(* slow reduction function *)
(*****************************************************************)
-open Entries
-open Decl_kinds
open Declare
+open DeclareDef
let definition_message = Declare.definition_message
-let save id const ?hook uctx (locality,_,kind) =
- let fix_exn = Future.fix_exn_of const.const_entry_body in
+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 ->
let k = Kindops.logical_kind_of_goal_kind kind in
@@ -134,10 +133,10 @@ let save id const ?hook uctx (locality,_,kind) =
VarRef id
| Global local ->
let k = Kindops.logical_kind_of_goal_kind kind in
- let kn = declare_constant id ~local (DefinitionEntry const, k) in
+ let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
ConstRef kn
in
- Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
+ DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
definition_message id
let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 4078c34331..45d332031f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -44,10 +44,11 @@ val jmeq_refl : unit -> EConstr.constr
val save
: Id.t
- -> Evd.side_effects Entries.definition_entry
- -> ?hook:Lemmas.declaration_hook
+ -> Evd.side_effects Proof_global.proof_entry
+ -> ?hook:DeclareDef.Hook.t
-> UState.t
- -> Decl_kinds.goal_kind
+ -> DeclareDef.locality
+ -> Decl_kinds.goal_object_kind
-> unit
(* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e7e523bb32..587e1fc2e8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -786,7 +786,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
Array.of_list
(List.map
(fun entry ->
- (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
+ (EConstr.of_constr (fst (fst(Future.force entry.Proof_global.proof_entry_body))), EConstr.of_constr (Option.get entry.Proof_global.proof_entry_type ))
)
(make_scheme evd (Array.map_to_list (fun const -> const,Sorts.InType) funs))
)
@@ -803,11 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
i*)
let lem_id = mk_correct_id f_id in
let (typ,_) = lemmas_types_infos.(i) in
+ let info = Lemmas.Info.make
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
let lemma = Lemmas.start_lemma
- lem_id
- Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
- !evd
- typ in
+ ~name:lem_id
+ ~poly:false
+ ~info
+ !evd
+ typ in
let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))) lemma in
@@ -865,12 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
Ensures by: obvious
i*)
let lem_id = mk_complete_id f_id in
- let lemma = Lemmas.start_lemma lem_id
- Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
- (fst lemmas_types_infos.(i)) in
+ let info = Lemmas.Info.make
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+ ~kind:Decl_kinds.(Proof Theorem) () in
+ let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
+ 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
+ (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+ (proving_tac i))) lemma) in
let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli
index 8394ac2823..96601785b6 100644
--- a/plugins/funind/invfun.mli
+++ b/plugins/funind/invfun.mli
@@ -15,5 +15,5 @@ val invfun :
val derive_correctness :
(Evd.evar_map ref ->
(Constr.pconstant * Sorts.family) list ->
- 'a Entries.definition_entry list) ->
+ 'a Proof_global.proof_entry list) ->
Constr.pconstant list -> Names.inductive list -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1ee5407bcc..425e498330 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -17,7 +17,6 @@ open EConstr
open Vars
open Namegen
open Environ
-open Entries
open Pp
open Names
open Libnames
@@ -1368,10 +1367,13 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
in
Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
in
+ let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
+ () in
let lemma = Lemmas.start_lemma
- na
- Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
- sigma gls_type ~hook:(Lemmas.mk_hook hook) in
+ ~name:na
+ ~poly:false (* FIXME *) ~info
+ sigma gls_type in
let lemma = if Indfun_common.is_strict_tcc ()
then
fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1409,9 +1411,13 @@ let com_terminate
nb_args ctx
hook =
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
- let lemma = Lemmas.start_lemma thm_name
- (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 info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+ let lemma = Lemmas.start_lemma ~name:thm_name
+ ~poly:false (*FIXME*)
+ ~sign:(Environ.named_context_val env)
+ ~info
+ ctx
+ (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in
fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
input_type relation rec_arg_num ))) lemma
@@ -1456,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 eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+ let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd
(EConstr.of_constr equation_lemma_type) in
let lemma = fst @@ Lemmas.by
(Proofview.V82.tactic (start_equation f_ref terminate_ref
@@ -1592,5 +1598,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
term_id
using_lemmas
(List.length res_vars)
- evd (Lemmas.mk_hook hook))
+ evd (DeclareDef.Hook.make hook))
()
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 49d8ab4e23..1e2b23bf96 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
if poly then ctx
else (* This is a global universe context that shouldn't be
refreshed at every use of the hint, declare it globally. *)
- (Declare.declare_universe_context false ctx;
+ (Declare.declare_universe_context ~poly:false ctx;
Univ.ContextSet.empty)
in
CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b8f4f5069..8acb29ba74 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,7 +1795,7 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance atts binders (name,t) fields =
- let _id = Classes.new_instance atts.polymorphic
+ let _id = Classes.new_instance ~poly:atts.polymorphic
name binders t (true, CAst.make @@ CRecord (fields))
~global:atts.global ~generalize:false Hints.empty_hint_info
in
@@ -1902,7 +1902,7 @@ let declare_projection n instance_id r =
Declare.definition_entry ~types:typ ~univs term
in
ignore(Declare.declare_constant n
- (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
+ (Declare.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
let build_morphism_signature env sigma m =
let m,ctx = Constrintern.interp_constr env sigma m in
@@ -1978,8 +1978,8 @@ let add_morphism_as_parameter atts m n : unit =
let evd = Evd.from_env env in
let uctx, instance = build_morphism_signature env evd m in
let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
- let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
- (Entries.ParameterEntry
+ let cst = Declare.declare_constant instance_id
+ (Declare.ParameterEntry
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
@@ -1994,9 +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,
- Decl_kinds.DefinitionBody Decl_kinds.Instance
- in
+ let poly = atts.polymorphic in
+ let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
| Globnames.ConstRef cst ->
@@ -2006,10 +2005,11 @@ let add_morphism_interactive atts m n : Lemmas.t =
declare_projection n instance_id (ConstRef cst)
| _ -> assert false
in
- let hook = Lemmas.mk_hook hook in
+ let hook = DeclareDef.Hook.make hook in
+ let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~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 =
@@ -2023,7 +2023,7 @@ let add_morphism atts binders m s n =
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
let _id, lemma = Classes.new_instance_interactive
- ~global:atts.global atts.polymorphic
+ ~global:atts.global ~poly:atts.polymorphic
instance_name binders instance_t
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9bbe339770..33798c43c8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
let open Constr in
let vars = CVars.universes_of_constr c in
let univs = UState.restrict_universe_context univs vars in
- let () = Declare.declare_universe_context false univs in
+ let () = Declare.declare_universe_context ~poly:false univs in
let types = (Typeops.infer (Global.env ()) c).uj_type in
let univs = Monomorphic_entry Univ.ContextSet.empty in
mkConst(declare_constant (Id.of_string na)
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 23:25:36 +0000