From 8abacf00c6c39ec98085d531737d18edc9c19b2a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 2 May 2019 19:46:02 +0200 Subject: Proof_global: pass only 1 pstate when we don't want the proof stack Typically instead of [start_proof : ontop:Proof_global.t option -> bla -> Proof_global.t] we have [start_proof : bla -> Proof_global.pstate] and the pstate is pushed on the stack by a caller around the vernacentries/mlg level. Naming can be a bit awkward, hopefully it can be improved (maybe in a followup PR). We can see some patterns appear waiting for nicer combinators, eg in mlg we often only want to work with the current proof, not the stack. Behaviour should be similar modulo bugs, let's see what CI says. --- plugins/derive/derive.ml | 4 ++-- plugins/derive/derive.mli | 2 +- plugins/derive/g_derive.mlg | 2 +- plugins/extraction/extract_env.ml | 4 ---- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/g_extraction.mlg | 8 ++++++- plugins/funind/functional_principles_proofs.ml | 9 ++++---- plugins/funind/functional_principles_types.ml | 11 +++++---- plugins/funind/g_indfun.mlg | 18 ++++++++------- plugins/funind/indfun.ml | 31 +++++++++++++++----------- plugins/funind/indfun.mli | 6 ++--- plugins/funind/invfun.ml | 8 +++---- plugins/funind/recdef.ml | 20 ++++++++--------- plugins/funind/recdef.mli | 4 +--- plugins/ltac/extratactics.mlg | 2 +- plugins/ltac/g_obligations.mlg | 4 ++-- plugins/ltac/g_rewrite.mlg | 3 ++- plugins/ltac/rewrite.ml | 6 ++--- plugins/ltac/rewrite.mli | 2 +- 19 files changed, 77 insertions(+), 69 deletions(-) (limited to 'plugins') 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 -- cgit v1.2.3