aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/extraction/extract_env.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml9
-rw-r--r--plugins/funind/gen_principle.ml16
-rw-r--r--plugins/funind/recdef.ml24
-rw-r--r--plugins/ltac/rewrite.ml4
6 files changed, 28 insertions, 29 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 7779e4f4c7..d85d3bd744 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -41,6 +41,6 @@ let start_deriving f suchthat name : Declare.Proof.t =
in
let info = Declare.Info.make ~proof_ending:(Declare.Proof_ending.(End_derive {f; name})) ~kind () in
- let lemma = Declare.start_dependent_proof ~name ~poly ~info goals in
+ let lemma = Declare.Proof.start_dependent ~name ~poly ~info goals in
Declare.Proof.map lemma ~f:(fun p ->
Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p)
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39c6c4ea54..af43c0517e 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -730,7 +730,7 @@ let extract_and_compile l =
let show_extraction ~pstate =
init ~inner:true false false;
let prf = Declare.Proof.get pstate in
- let sigma, env = Declare.get_current_context pstate in
+ let sigma, env = Declare.Proof.get_current_context pstate in
let trms = Proof.partial_proof prf in
let extr_term t =
let ast, ty = extract_constr env sigma t in
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 2c85ae079f..79f311e282 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -855,13 +855,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
constructing the lemma Ensures by: obvious i*)
let info = Declare.Info.make () in
let lemma =
- Declare.start_proof ~name:(mk_equation_id f_id) ~poly:false ~info
+ Declare.Proof.start ~name:(mk_equation_id f_id) ~poly:false ~info
~impargs:[] evd lemma_type
in
- let lemma, _ = Declare.by (Proofview.V82.tactic prove_replacement) lemma in
+ let lemma, _ =
+ Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
+ in
let () =
- Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
in
evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index a914cef6e4..50ce783579 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1520,15 +1520,15 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let typ, _ = lemmas_types_infos.(i) in
let info = Declare.Info.make () in
let lemma =
- Declare.start_proof ~name:lem_id ~poly:false ~info ~impargs:[] !evd
+ Declare.Proof.start ~name:lem_id ~poly:false ~info ~impargs:[] !evd
typ
in
let lemma =
- fst @@ Declare.by (Proofview.V82.tactic (proving_tac i)) lemma
+ fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
in
let () =
- Declare.save_lemma_proved ~proof:lemma
- ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
@@ -1586,12 +1586,12 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
let lem_id = mk_complete_id f_id in
let info = Declare.Info.make () in
let lemma =
- Declare.start_proof ~name:lem_id ~poly:false sigma ~info ~impargs:[]
+ Declare.Proof.start ~name:lem_id ~poly:false sigma ~info ~impargs:[]
(fst lemmas_types_infos.(i))
in
let lemma =
fst
- (Declare.by
+ (Declare.Proof.by
(Proofview.V82.tactic
(observe_tac
("prove completeness (" ^ Id.to_string f_id ^ ")")
@@ -1599,8 +1599,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
lemma)
in
let () =
- Declare.save_lemma_proved ~proof:lemma
- ~opaque:Vernacexpr.Transparent ~idopt:None
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
+ ~idopt:None
in
let finfo =
match find_Function_infos (fst f_as_constant) with
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9f36eada45..5a188ca82b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,8 +58,7 @@ let declare_fun name kind ?univs value =
(Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
let defined lemma =
- Declare.save_lemma_proved ~proof:lemma ~opaque:Vernacexpr.Transparent
- ~idopt:None
+ Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
let def_of_const t =
match Constr.kind t with
@@ -1490,19 +1489,19 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
[Hints.Hint_db.empty TransparentState.empty false] ]))
in
let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
- Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None
+ Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
in
let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
let lemma =
- Declare.start_proof ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
+ Declare.Proof.start ~name:na ~poly:false (* FIXME *) ~info ~impargs:[] sigma
gls_type
in
let lemma =
if Indfun_common.is_strict_tcc () then
- fst @@ Declare.by (Proofview.V82.tactic tclIDTAC) lemma
+ fst @@ Declare.Proof.by (Proofview.V82.tactic tclIDTAC) lemma
else
fst
- @@ Declare.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic (fun g ->
tclTHEN decompose_and_tac
(tclORELSE
@@ -1533,18 +1532,18 @@ let com_terminate interactive_proof tcc_lemma_name tcc_lemma_ref is_mes
let start_proof env ctx tac_start tac_end =
let info = Declare.Info.make ~hook () in
let lemma =
- Declare.start_proof ~name:thm_name ~poly:false (*FIXME*) ~info ctx
+ Declare.Proof.start ~name:thm_name ~poly:false (*FIXME*) ~info ctx
~impargs:[]
(EConstr.of_constr (compute_terminate_type nb_args fonctional_ref))
in
let lemma =
fst
- @@ Declare.by
+ @@ Declare.Proof.by
(New.observe_tac (fun _ _ -> str "starting_tac") tac_start)
lemma
in
fst
- @@ Declare.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic
(observe_tac
(fun _ _ -> str "whole_start")
@@ -1607,12 +1606,12 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
let equation_lemma_type = subst1 f_constr equation_lemma_type in
let info = Declare.Info.make () in
let lemma =
- Declare.start_proof ~name:eq_name ~poly:false evd ~info ~impargs:[]
+ Declare.Proof.start ~name:eq_name ~poly:false evd ~info ~impargs:[]
(EConstr.of_constr equation_lemma_type)
in
let lemma =
fst
- @@ Declare.by
+ @@ Declare.Proof.by
(Proofview.V82.tactic
(start_equation f_ref terminate_ref (fun x ->
prove_eq
@@ -1646,8 +1645,7 @@ let com_eqn uctx nb_arg eq_name functional_ref f_ref terminate_ref
in
let _ =
Flags.silently
- (fun () ->
- Declare.save_lemma_proved ~proof:lemma ~opaque:opacity ~idopt:None)
+ (fun () -> Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None)
()
in
()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 0c1c763b64..405fe7b844 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2000,8 +2000,8 @@ let add_morphism_interactive atts m n : Declare.Proof.t =
let info = Declare.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Declare.start_proof ~name:instance_id ~poly ~info ~impargs:[] evd morph in
- fst (Declare.by (Tacinterp.interp tac) lemma)) ()
+ let lemma = Declare.Proof.start ~name:instance_id ~poly ~info ~impargs:[] evd morph in
+ fst (Declare.Proof.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
init_setoid ();
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:45:27 +0000