aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml4
-rw-r--r--plugins/derive/derive.mli2
-rw-r--r--plugins/derive/g_derive.mlg2
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--plugins/extraction/extract_env.mli2
-rw-r--r--plugins/extraction/g_extraction.mlg8
-rw-r--r--plugins/funind/functional_principles_proofs.ml9
-rw-r--r--plugins/funind/functional_principles_types.ml11
-rw-r--r--plugins/funind/g_indfun.mlg18
-rw-r--r--plugins/funind/indfun.ml31
-rw-r--r--plugins/funind/indfun.mli6
-rw-r--r--plugins/funind/invfun.ml8
-rw-r--r--plugins/funind/recdef.ml20
-rw-r--r--plugins/funind/recdef.mli4
-rw-r--r--plugins/ltac/extratactics.mlg2
-rw-r--r--plugins/ltac/g_obligations.mlg4
-rw-r--r--plugins/ltac/g_rewrite.mlg3
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--plugins/ltac/rewrite.mli2
19 files changed, 77 insertions, 69 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4769c2dc53..9c1882dc9a 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -101,8 +101,8 @@ let start_deriving f suchthat lemma =
in
let terminator = Proof_global.make_terminator terminator in
- let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
- Proof_global.simple_with_current_proof begin fun _ p ->
+ let pstate = Proof_global.start_dependent_proof lemma kind goals terminator in
+ Proof_global.modify_proof begin fun p ->
let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
p
end pstate
diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli
index 6bb923118e..6e4bffa0b6 100644
--- a/plugins/derive/derive.mli
+++ b/plugins/derive/derive.mli
@@ -12,4 +12,4 @@
(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]
and [lemma] as the proof. *)
-val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.t
+val start_deriving : Names.Id.t -> Constrexpr.constr_expr -> Names.Id.t -> Proof_global.pstate
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index 214a9d8bb5..ee076f5ae3 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -24,5 +24,5 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
| ![ proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
- { fun ~pstate -> Some Derive.(start_deriving f suchthat lemma) }
+ { fun ~pstate -> Some (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) }
END
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 8f17f7b2dd..c5439ffaf6 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -751,10 +751,6 @@ let extract_and_compile l =
(* Show the extraction of the current ongoing proof *)
let show_extraction ~pstate =
- let pstate = match pstate with
- | None -> CErrors.user_err Pp.(str "No ongoing proof")
- | Some pstate -> pstate
- in
init ~inner:true false false;
let prf = Proof_global.give_me_the_proof pstate in
let sigma, env = Pfedit.get_current_context pstate in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7ba7e05019..efd5b5575f 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -40,4 +40,4 @@ val structure_for_compute :
(* Show the extraction of the current ongoing proof *)
-val show_extraction : pstate:Proof_global.t option -> unit
+val show_extraction : pstate:Proof_global.pstate -> unit
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index db1a389fe7..d43d90af60 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -179,5 +179,11 @@ END
VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
| ![ proof ] [ "Show" "Extraction" ]
- -> { fun ~pstate -> let () = show_extraction ~pstate in pstate }
+ -> { fun ~pstate:ontop ->
+ let pstate = Option.map Proof_global.get_current_pstate ontop in
+ let pstate = match pstate with
+ | None -> CErrors.user_err Pp.(str "No ongoing proof")
+ | Some pstate -> pstate
+ in
+ let () = show_extraction ~pstate in ontop }
END
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f2b9ba2ec6..e38ea992ab 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,7 +990,7 @@ 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 pstate = Lemmas.start_proof ~ontop:None
+ let pstate = Lemmas.start_proof
(*i The next call to mk_equation_id is valid since we are constructing the lemma
Ensures by: obvious
i*)
@@ -1000,8 +1000,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
lemma_type
in
let pstate,_ = Pfedit.by (Proofview.V82.tactic prove_replacement) pstate in
- let pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
- pstate, evd
+ let ontop = Proof_global.push ~ontop:None pstate in
+ ignore(Lemmas.save_proof_proved ?proof:None ~ontop ~opaque:Proof_global.Transparent ~idopt:None);
+ evd
let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num all_funs g =
@@ -1015,7 +1016,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
Ensures by: obvious
i*)
let equation_lemma_id = (mk_equation_id f_id) in
- evd := snd @@ generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
+ evd := generate_equation_lemma !evd all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
let _ =
match e with
| Option.IsNone ->
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 2c107d39d9..7b26cb0c74 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -309,7 +309,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
evd := sigma;
let hook = Lemmas.mk_hook (hook new_principle_type) in
let pstate =
- Lemmas.start_proof ~ontop:None
+ Lemmas.start_proof
new_princ_name
(Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.Theorem))
!evd
@@ -328,8 +328,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
let { id; entries; persistence } = fst @@ close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pstate in
match entries with
| [entry] ->
- let pstate = discard_current pstate in
- (id,(entry,persistence)), hook, pstate
+ (id,(entry,persistence)), hook
| _ ->
CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
@@ -381,7 +380,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,pstate) =
+ let ((id,(entry,g_kind)),hook) =
build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
proof_tac hook
in
@@ -520,7 +519,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
s::l_schemes -> s,l_schemes
| _ -> anomaly (Pp.str "")
in
- let ((_,(const,_)),_,pstate) =
+ let ((_,(const,_)),_) =
try
build_functional_principle evd false
first_type
@@ -580,7 +579,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Safe_typing.private_
(* If we reach this point, the two principle are not mutually recursive
We fall back to the previous method
*)
- let ((_,(const,_)),_,pstate) =
+ let ((_,(const,_)),_) =
build_functional_principle
evd
false
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index dbfc0fc91d..b8db3dc5ce 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -190,7 +190,9 @@ VERNAC COMMAND EXTEND Function
| Vernacextend.VtSideff ids, _ when hard ->
Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
| x -> x }
- -> { do_generate_principle false (List.map snd recsl) }
+ -> { fun ~pstate:ontop ->
+ let pstate = do_generate_principle false (List.map snd recsl) in
+ Proof_global.maybe_push ~ontop pstate}
END
{
@@ -228,30 +230,30 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
=> { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
->
- { fun ~pstate ->
+ { fun ~pstate:ontop ->
begin
try
- Functional_principles_types.build_scheme fas; pstate
+ Functional_principles_types.build_scheme fas; ontop
with
| Functional_principles_types.No_graph_found ->
begin
match fas with
| (_,fun_name,_)::_ ->
begin
- let pstate = make_graph ~pstate (Smartlocate.global_with_alias fun_name) in
- try Functional_principles_types.build_scheme fas; pstate
+ let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in
+ try Functional_principles_types.build_scheme fas; ontop
with
| Functional_principles_types.No_graph_found ->
CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
| e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
- warning_error names e; pstate
+ warning_error names e; ontop
end
| _ -> assert false (* we can only have non empty list *)
end
| e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
- warning_error names e; pstate
+ warning_error names e; ontop
end
}
END
@@ -266,5 +268,5 @@ END
(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
- { make_graph (Smartlocate.global_with_alias c) }
+ { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) }
END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a6b088de0c..d47c12a7cb 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -410,7 +410,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
with e when CErrors.noncritical e ->
on_error names e
-let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
+let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
match fixpoint_exprl with
| [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec ->
let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
@@ -432,9 +432,9 @@ let register_struct ~pstate is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * V
(Evd.from_env (Global.env ()),[])
fixpoint_exprl
in
- pstate, evd,List.rev rev_pconstants
+ None, evd,List.rev rev_pconstants
| _ ->
- let pstate = ComFixpoint.do_fixpoint ~ontop:pstate Global false fixpoint_exprl in
+ let pstate = ComFixpoint.do_fixpoint Global false fixpoint_exprl in
let evd,rev_pconstants =
List.fold_left
(fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
@@ -633,8 +633,8 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
fixpoint_exprl_with_new_bl
-let do_generate_principle ~pstate pconstants on_error register_built interactive_proof
- (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.t option =
+let do_generate_principle pconstants on_error register_built interactive_proof
+ (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) : Proof_global.pstate option =
List.iter (fun (_,l) -> if not (List.is_empty l) then error "Function does not support notations for now") fixpoint_exprl;
let pstate, _is_struct =
match fixpoint_exprl with
@@ -661,7 +661,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
in
if register_built
then register_wf name rec_impls wf_rel wf_x.CAst.v using_lemmas args types body pre_hook, false
- else pstate, false
+ else None, false
|[((_,Some {CAst.v = Constrexpr.CMeasureRec(wf_x,wf_mes,wf_rel_opt)},_,_,_),_) as fixpoint_expr] ->
let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr =
match recompute_binder_list [fixpoint_expr] with
@@ -685,7 +685,7 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
in
if register_built
then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook, true
- else pstate, true
+ else None, true
| _ ->
List.iter (function ((_na,ord,_args,_body,_type),_not) ->
match ord with
@@ -704,8 +704,8 @@ let do_generate_principle ~pstate pconstants on_error register_built interactive
let is_rec = List.exists (is_rec fix_names) recdefs in
let pstate,evd,pconstants =
if register_built
- then register_struct ~pstate is_rec fixpoint_exprl
- else pstate, Evd.from_env (Global.env ()), pconstants
+ then register_struct is_rec fixpoint_exprl
+ else None, Evd.from_env (Global.env ()), pconstants
in
let evd = ref evd in
generate_principle
@@ -839,9 +839,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
| _ -> [],b,t
-let make_graph ~pstate (f_ref : GlobRef.t) =
- let sigma, env = Option.cata Pfedit.get_current_context
- (let e = Global.env () in Evd.from_env e, e) pstate in
+let make_graph env sigma (f_ref : GlobRef.t) =
let c,c_body =
match f_ref with
| ConstRef c ->
@@ -902,11 +900,18 @@ let make_graph ~pstate (f_ref : GlobRef.t) =
[((CAst.make id,None),None,nal_tas,t,Some b),[]]
in
let mp = Constant.modpath c in
- let pstate = do_generate_principle ~pstate [c,Univ.Instance.empty] error_error false false expr_list in
+ let pstate = do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list in
(* We register the infos *)
List.iter
(fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make2 mp (Label.of_id id)))
expr_list;
pstate)
+let make_graph ~ontop f_ref =
+ let pstate = Option.map Proof_global.get_current_pstate ontop in
+ let sigma, env = Option.cata Pfedit.get_current_context
+ (let e = Global.env () in Evd.from_env e, e) pstate in
+ Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop
+ (make_graph env sigma f_ref)
+
let do_generate_principle = do_generate_principle [] warning_error true
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index acf85f539e..cf4ef23d1a 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -5,10 +5,10 @@ val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit
val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit
-val do_generate_principle : pstate:Proof_global.t option ->
+val do_generate_principle :
bool ->
(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
- Proof_global.t option
+ Proof_global.pstate option
val functional_induction :
bool ->
@@ -17,4 +17,4 @@ val functional_induction :
Ltac_plugin.Tacexpr.or_and_intro_pattern option ->
Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
-val make_graph : pstate:Proof_global.t option -> GlobRef.t -> Proof_global.t option
+val make_graph : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2a0140f02c..03568fc6c7 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,7 +803,7 @@ 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 pstate = Lemmas.start_proof ~ontop:None
+ let pstate = Lemmas.start_proof
lem_id
(Decl_kinds.Global,false,((Decl_kinds.Proof Decl_kinds.Theorem)))
!evd
@@ -811,7 +811,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
let pstate = fst @@ Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))) pstate in
- let _ = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+ let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
@@ -865,13 +865,13 @@ 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 pstate = Lemmas.start_proof ~ontop:None lem_id
+ let pstate = Lemmas.start_proof lem_id
(Decl_kinds.Global,false,(Decl_kinds.Proof Decl_kinds.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)^")")
(proving_tac i))) pstate) in
- let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
+ let () = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None in
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index de1b592337..b4d0f092d8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value =
let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let defined pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Transparent ~idopt:None
+let defined pstate = Lemmas.save_pstate_proved ~pstate ~opaque:Proof_global.Transparent ~idopt:None
let def_of_const t =
match (Constr.kind t) with
@@ -1367,10 +1367,9 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
)
g)
in
- let _pstate = Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None in
- ()
+ Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None
in
- let pstate = Lemmas.start_proof ~ontop:(Some pstate)
+ let pstate = Lemmas.start_proof
na
(Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
sigma gls_type ~hook:(Lemmas.mk_hook hook) in
@@ -1399,7 +1398,7 @@ let open_new_goal pstate build_proof sigma using_lemmas ref_ goal_name (gls_type
try
Some (fst @@ by (Proofview.V82.tactic tclIDTAC) pstate) (* raises UserError _ if the proof is complete *)
with UserError _ ->
- defined pstate
+ (defined pstate; None)
let com_terminate
tcc_lemma_name
@@ -1413,7 +1412,7 @@ let com_terminate
nb_args ctx
hook =
let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
- let pstate = Lemmas.start_proof ~ontop:None thm_name
+ let pstate = Lemmas.start_proof thm_name
(Global, 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
@@ -1431,7 +1430,8 @@ let com_terminate
with EmptySubgoals ->
(* a non recursive function declared with measure ! *)
tcc_lemma_ref := Not_needed;
- defined pstate
+ defined pstate;
+ None
let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
(cont_tactic:Id.t list -> tactic) g =
@@ -1459,7 +1459,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 ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd
+ let pstate = Lemmas.start_proof eq_name (Global, 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
@@ -1489,13 +1489,13 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
}
)
)) pstate in
- let _ = Flags.silently (fun () -> Lemmas.save_proof_proved ?proof:None ~pstate ~opaque:opacity ~idopt:None) () in
+ let _ = Flags.silently (fun () -> Lemmas.save_pstate_proved ~pstate ~opaque:opacity ~idopt:None) () in
()
(* Pp.msgnl (fun _ _ -> str "eqn finished"); *)
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
- generate_induction_principle using_lemmas : Proof_global.t option =
+ generate_induction_principle using_lemmas : Proof_global.pstate option =
let open Term in
let open Constr in
let open CVars in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index a006c2c354..84d7a399e1 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -14,6 +14,4 @@ bool ->
int -> Constrexpr.constr_expr -> (pconstant ->
Indfun_common.tcc_lemma_value ref ->
pconstant ->
- pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.t option
-
-
+ pconstant -> int -> EConstr.types -> int -> EConstr.constr -> unit) -> Constrexpr.constr_expr list -> Proof_global.pstate option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4c186dce09..5e4969567d 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1118,7 +1118,7 @@ END
VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { fun ~pstate -> Option.map Proof_global.compact_the_proof pstate }
+ { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index de3a9c9fa9..d7918a58ac 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,8 +80,8 @@ GRAMMAR EXTEND Gram
open Obligations
-let obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.obligation ~ontop:pstate obl t) tac)
-let next_obligation ~pstate obl tac = Some (with_tac (fun t -> Obligations.next_obligation ~ontop:pstate obl t) tac)
+let obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.obligation obl t) tac))
+let next_obligation ~pstate obl tac = Some (Proof_global.push ~ontop:pstate (with_tac (fun t -> Obligations.next_obligation obl t) tac))
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 2fad1f6b6a..e3f4b8ef59 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -280,7 +280,8 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
(* This command may or may not open a goal *)
=> { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
-> {
- add_morphism_infer atts m n
+ fun ~pstate:ontop ->
+ Option.cata (fun ps -> Some (Proof_global.push ~ontop ps)) ontop (add_morphism_infer atts m n)
}
| #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> { VtStartProof(GuaranteesOpacity,[n]), VtLater }
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 6f84e6c18d..efca411754 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1974,7 +1974,7 @@ let warn_add_morphism_deprecated =
CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () ->
Pp.(str "Add Morphism f : id is deprecated, please use Add Morphism f with signature (...) as id"))
-let add_morphism_infer ~pstate atts m n : Proof_global.t option =
+let add_morphism_infer atts m n : Proof_global.pstate option =
warn_add_morphism_deprecated ?loc:m.CAst.loc ();
init_setoid ();
let instance_id = add_suffix n "_Proper" in
@@ -1991,7 +1991,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
add_instance (Classes.mk_instance
(PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
declare_projection n instance_id (ConstRef cst);
- pstate
+ None
else
let kind = Decl_kinds.Global, atts.polymorphic,
Decl_kinds.DefinitionBody Decl_kinds.Instance
@@ -2008,7 +2008,7 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
let hook = Lemmas.mk_hook hook in
Flags.silently
(fun () ->
- let pstate = Lemmas.start_proof ~ontop:pstate ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let pstate = Lemmas.start_proof ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
Some (fst Pfedit.(by (Tacinterp.interp tac) pstate))) ()
let add_morphism ~pstate atts binders m s n =
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index a200cb5ced..cab7d0065e 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -89,7 +89,7 @@ val add_setoid : pstate:Proof_global.t option ->
rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr ->
Id.t -> Proof_global.t option
-val add_morphism_infer : pstate:Proof_global.t option -> rewrite_attributes -> constr_expr -> Id.t -> Proof_global.t option
+val add_morphism_infer : rewrite_attributes -> constr_expr -> Id.t -> Proof_global.pstate option
val add_morphism : pstate:Proof_global.t option ->
rewrite_attributes -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> Proof_global.t option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:47:55 +0000