aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/functional_principles_types.ml6
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml6
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/invfun.ml4
-rw-r--r--plugins/funind/recdef.ml11
7 files changed, 16 insertions, 17 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f773b2c39e..6a5307d8f5 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -992,7 +992,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* 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
+ ~kind:(Decls.(Proof Theorem)) () in
let lemma = Lemmas.start_lemma
(*i The next call to mk_equation_id is valid since we are constructing the lemma
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 3bab750534..87910eeae7 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -371,7 +371,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
Declare.declare_constant
name
(Declare.DefinitionEntry ce,
- Decl_kinds.IsDefinition (Decl_kinds.Scheme))
+ Decls.(IsDefinition Scheme))
);
Declare.definition_message name;
names := name :: !names
@@ -387,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 (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
+ save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decls.(Proof Theorem)
with e when CErrors.noncritical e ->
raise (Defining_principle e)
@@ -638,7 +638,7 @@ let build_scheme fas =
ignore
(Declare.declare_constant
princ_id
- (Declare.DefinitionEntry def_entry,Decl_kinds.IsProof Decl_kinds.Theorem));
+ (Declare.DefinitionEntry def_entry,Decls.(IsProof Theorem)));
Declare.definition_message princ_id
)
fas
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d305a58ccc..9a9e0b9692 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -419,7 +419,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
~name:fname
~poly:false
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
- ~kind:Decl_kinds.Definition pl
+ ~kind:Decls.Definition pl
bl None body (Some ret_type);
let evd,rev_pconstants =
List.fold_left
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 56ed406e2f..b32b27ebeb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -127,13 +127,13 @@ let save id const ?hook uctx scope kind =
let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
let r = match scope with
| Discharge ->
- let k = Kindops.logical_kind_of_goal_kind kind in
+ let k = Decls.logical_kind_of_goal_kind kind in
let c = SectionLocalDef const in
let _ = declare_variable id (Lib.cwd(), c, k) in
VarRef id
| Global local ->
- let k = Kindops.logical_kind_of_goal_kind kind in
- let kn = declare_constant id ~local (Declare.DefinitionEntry const, k) in
+ let k = Decls.logical_kind_of_goal_kind kind in
+ let kn = declare_constant id ~local (DefinitionEntry const, k) in
ConstRef kn
in
DeclareDef.Hook.(call ?hook ~fix_exn { S.uctx; obls = []; scope; dref = r });
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 45d332031f..1758efe584 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -48,7 +48,7 @@ val save
-> ?hook:DeclareDef.Hook.t
-> UState.t
-> DeclareDef.locality
- -> Decl_kinds.goal_object_kind
+ -> Decls.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 86defb2f2f..153b27c855 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 info = Lemmas.Info.make
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
- ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+ ~kind:(Decls.(Proof Theorem)) () in
let lemma = Lemmas.start_lemma
~name:lem_id
~poly:false
@@ -871,7 +871,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let lem_id = mk_complete_id f_id in
let info = Lemmas.Info.make
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
- ~kind:Decl_kinds.(Proof Theorem) () in
+ ~kind:Decls.(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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d38e28c0e7..0398acf242 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -30,7 +30,6 @@ open Tacmach
open Tactics
open Nametab
open Declare
-open Decl_kinds
open Tacred
open Goal
open Glob_term
@@ -196,7 +195,7 @@ let (value_f: Constr.t list -> GlobRef.t -> Constr.t) =
let body = EConstr.Unsafe.to_constr body in
it_mkLambda_or_LetIn body context
-let (declare_f : Id.t -> logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
+let (declare_f : Id.t -> Decls.logical_kind -> Constr.t list -> GlobRef.t -> GlobRef.t) =
fun f_id kind input_type fterm_ref ->
declare_fun f_id kind (value_f input_type fterm_ref);;
@@ -1368,7 +1367,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
Lemmas.save_lemma_proved ~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)
+ ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decls.(Proof Lemma))
() in
let lemma = Lemmas.start_lemma
~name:na
@@ -1411,7 +1410,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
- let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+ let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:Decls.(Proof Lemma) () in
let lemma = Lemmas.start_lemma ~name:thm_name
~poly:false (*FIXME*)
~sign:(Environ.named_context_val env)
@@ -1535,7 +1534,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
let term_id = add_suffix function_name "_terminate" in
let functional_ref =
let univs = Evd.univ_entry ~poly:false evd in
- declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~univs res
+ declare_fun functional_id Decls.(IsDefinition Definition) ~univs res
in
(* Refresh the global universes, now including those of _F *)
let evd = Evd.from_env (Global.env ()) in
@@ -1549,7 +1548,7 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
(* let _ = Pp.msgnl (fun _ _ -> str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook { DeclareDef.Hook.S.uctx ; _ } =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
- let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
+ let f_ref = declare_f function_name Decls.(IsProof Lemma) arg_types term_ref in
let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in
(* message "start second proof"; *)
let stop =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:51:38 +0000