aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coqpp/coqpp_main.ml21
-rw-r--r--doc/plugin_tutorial/tuto1/src/g_tuto1.mlg16
-rw-r--r--plugins/derive/g_derive.mlg4
-rw-r--r--plugins/extraction/g_extraction.mlg10
-rw-r--r--plugins/funind/g_indfun.mlg25
-rw-r--r--plugins/funind/indfun.ml11
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/ltac/extratactics.mlg6
-rw-r--r--plugins/ltac/g_ltac.mlg8
-rw-r--r--plugins/ltac/g_obligations.mlg16
-rw-r--r--plugins/ltac/g_rewrite.mlg55
-rw-r--r--plugins/ltac/rewrite.ml67
-rw-r--r--plugins/ltac/rewrite.mli35
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg34
-rw-r--r--user-contrib/Ltac2/tac2entries.ml5
-rw-r--r--user-contrib/Ltac2/tac2entries.mli5
-rw-r--r--user-contrib/Ltac2/tac2expr.mli2
-rw-r--r--vernac/classes.ml15
-rw-r--r--vernac/classes.mli5
-rw-r--r--vernac/vernacentries.ml11
-rw-r--r--vernac/vernacentries.mli4
-rw-r--r--vernac/vernacstate.ml2
-rw-r--r--vernac/vernacstate.mli2
23 files changed, 188 insertions, 173 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 42fe13e4eb..8444f3a58c 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -359,10 +359,29 @@ let print_atts_right fmt = function
let print_body_wrapper fmt r =
match r.vernac_state with
- | Some "proof" ->
+ | Some "proof_stack" ->
fprintf fmt "let proof = (%a) ~pstate:st.Vernacstate.proof in { st with Vernacstate.proof }" print_code r.vernac_body
+
+ | Some "open_proof" ->
+ let push = "Some (Proof_global.push ~ontop:st.Vernacstate.proof pstate)" in
+ fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
+
+ | Some "maybe_open_proof" ->
+ let push = "Proof_global.maybe_push ~ontop:st.Vernacstate.proof pstate" in
+ fprintf fmt "let pstate = (%a) in let proof = %s in { st with Vernacstate.proof }" print_code r.vernac_body push
+
+ | Some "proof" ->
+ fprintf fmt "let proof = Vernacentries.modify_pstate ~pstate:st.Vernacstate.proof (%a) in { st with Vernacstate.proof }" print_code r.vernac_body
+
+ | Some "proof_opt_query" ->
+ fprintf fmt "let () = (%a) ~pstate:(Vernacstate.pstate st) in st" print_code r.vernac_body
+
+ | Some "proof_query" ->
+ fprintf fmt "let () = Vernacentries.with_pstate ~pstate:st.Vernacstate.proof (%a) in st" print_code r.vernac_body
+
| None ->
fprintf fmt "let () = %a in st" print_code r.vernac_body
+
| Some x ->
fatal ("unsupported state specifier: " ^ x)
diff --git a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
index 147b0df567..300d62285a 100644
--- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
+++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg
@@ -145,13 +145,11 @@ END
it gives an error message that is basically impossible to understand. *)
VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| ![ proof ] [ "Cmd9" ] ->
- { fun ~pstate:ontop ->
- Option.iter (fun ontop ->
- let pstate = Proof_global.get_current_pstate ontop in
- let sigma, env = Pfedit.get_current_context pstate in
- let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
- Feedback.msg_notice
- (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)) ontop;
- ontop }
+| ![ proof_query ] [ "Cmd9" ] ->
+ { fun ~pstate ->
+ let sigma, env = Pfedit.get_current_context pstate in
+ let pprf = Proof.partial_proof Proof_global.(give_me_the_proof pstate) in
+ Feedback.msg_notice
+ (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf)
+ }
END
diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index ee076f5ae3..d25b8fd01c 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -23,6 +23,6 @@ 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 (Proof_global.push ~ontop:pstate Derive.(start_deriving f suchthat lemma)) }
+| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+ { Derive.(start_deriving f suchthat lemma) }
END
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index d43d90af60..487accbc9b 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -178,12 +178,6 @@ END
(* Show the extraction of the current proof *)
VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof ] [ "Show" "Extraction" ]
- -> { 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 }
+| ![ proof_query ] [ "Show" "Extraction" ]
+ -> { show_extraction }
END
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index b8db3dc5ce..cc772e96f3 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -177,7 +177,7 @@ let () =
(* TASSI: n'importe quoi ! *)
VERNAC COMMAND EXTEND Function
-| ![ proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
=> { let hard = List.exists (function
| _,((_,(Some { CAst.v = CMeasureRec _ }
| Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -190,9 +190,7 @@ VERNAC COMMAND EXTEND Function
| Vernacextend.VtSideff ids, _ when hard ->
Vernacextend.(VtStartProof (GuaranteesOpacity, ids), VtLater)
| x -> x }
- -> { fun ~pstate:ontop ->
- let pstate = do_generate_principle false (List.map snd recsl) in
- Proof_global.maybe_push ~ontop pstate}
+ -> { do_generate_principle false (List.map snd recsl) }
END
{
@@ -227,33 +225,32 @@ let warning_error names e =
}
VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
=> { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
->
- { fun ~pstate:ontop ->
- begin
+ { begin
try
- Functional_principles_types.build_scheme fas; ontop
+ Functional_principles_types.build_scheme fas; None
with
| Functional_principles_types.No_graph_found ->
begin
match fas with
| (_,fun_name,_)::_ ->
begin
- let ontop = make_graph ~ontop (Smartlocate.global_with_alias fun_name) in
- try Functional_principles_types.build_scheme fas; ontop
+ let pstate = make_graph (Smartlocate.global_with_alias fun_name) in
+ try Functional_principles_types.build_scheme fas; pstate
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; ontop
+ warning_error names e; pstate
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; ontop
+ warning_error names e; None
end
}
END
@@ -267,6 +264,6 @@ END
(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ proof ] ["Generate" "graph" "for" reference(c)] ->
- { fun ~pstate:ontop -> make_graph ~ontop (Smartlocate.global_with_alias c) }
+| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+ { make_graph (Smartlocate.global_with_alias c) }
END
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d47c12a7cb..6ea2eb579f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -839,7 +839,9 @@ let rec get_args b t : Constrexpr.local_binder_expr list *
| _ -> [],b,t
-let make_graph env sigma (f_ref : GlobRef.t) =
+let make_graph (f_ref : GlobRef.t) =
+ let env = Global.env() in
+ let sigma = Evd.from_env env in
let c,c_body =
match f_ref with
| ConstRef c ->
@@ -907,11 +909,4 @@ let make_graph env sigma (f_ref : GlobRef.t) =
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 cf4ef23d1a..c803484617 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -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 : ontop:Proof_global.t option -> GlobRef.t -> Proof_global.t option
+val make_graph : GlobRef.t -> Proof_global.pstate option
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 5e4969567d..4a2fb425ac 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -934,7 +934,7 @@ END
VERNAC COMMAND EXTEND GrabEvars
| ![ proof ] [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p)) pstate }
+ -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -966,7 +966,7 @@ END
VERNAC COMMAND EXTEND Unshelve
| ![ proof ] [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Option.map (Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p)) pstate }
+ -> { fun ~pstate -> Proof_global.modify_proof (fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
@@ -1118,7 +1118,7 @@ END
VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { fun ~pstate -> Option.map Proof_global.(modify_current_pstate compact_the_proof) pstate }
+ { fun ~pstate -> Proof_global.compact_the_proof pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 7eb34158e8..9bf5bd1bda 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -376,7 +376,7 @@ let () = declare_int_option {
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Proof_global.with_current_proof (fun etac p ->
+ let pstate, status = Proof_global.with_proof (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
let info = Option.append info !print_info_trace in
@@ -388,7 +388,7 @@ let vernac_solve ~pstate n info tcom b =
let p = Proof.maximal_unfocus Vernacentries.command_focus p in
p,status) pstate in
if not status then Feedback.feedback Feedback.AddedAxiom;
- Some pstate
+ pstate
let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s
@@ -438,7 +438,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{ classify_as_proofstep } -> {
let g = Option.default (Goal_select.get_default_goal_selector ()) g in
- Vernacentries.vernac_require_open_proof vernac_solve g n t def
+ vernac_solve g n t def
}
| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
{
@@ -450,7 +450,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve
VtLater
} -> {
let t = rm_abstract t in
- Vernacentries.vernac_require_open_proof vernac_solve Goal_select.SelectAll n t def
+ vernac_solve Goal_select.SelectAll n t def
}
END
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index d7918a58ac..c01b97c14d 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -80,25 +80,25 @@ GRAMMAR EXTEND Gram
open Obligations
-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 obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac
+let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac
let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), VtLater)
}
VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, Some name, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
{ obligation (num, Some name, None) tac }
-| ![ proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
{ obligation (num, None, Some t) tac }
-| ![ proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
{ obligation (num, None, None) tac }
-| ![ proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
{ next_obligation (Some name) tac }
-| ![ proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
END
VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index e3f4b8ef59..bb29323858 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -180,34 +180,34 @@ TACTIC EXTEND setoid_rewrite
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] ->
{ declare_relation atts a aeq n None None None }
END
VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts a aeq n None None (Some lemma3) }
END
@@ -234,66 +234,59 @@ GRAMMAR EXTEND Gram
END
VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None None }
END
VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" ident(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
END
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
add_setoid atts [] a aeq t n
}
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
+ | #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] ->
{
add_setoid atts binders a aeq t n
}
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
+ | #[ atts = rewrite_attributes; ] ![ maybe_open_proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ]
(* This command may or may not open a goal *)
=> { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater }
- -> {
- 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) ]
+ -> { add_morphism_infer atts m n }
+ | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ]
=> { VtStartProof(GuaranteesOpacity,[n]), VtLater }
- -> {
- add_morphism atts [] m s n
- }
- | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
+ -> { add_morphism atts [] m s n }
+ | #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" ident(n) ]
=> { VtStartProof(GuaranteesOpacity,[n]), VtLater }
- -> {
- add_morphism atts binders m s n
- }
+ -> { add_morphism atts binders m s n }
END
TACTIC EXTEND setoid_symmetry
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index efca411754..5d57a2f27f 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -23,7 +23,6 @@ open Tacticals.New
open Tactics
open Pretype_errors
open Typeclasses
-open Classes
open Constrexpr
open Globnames
open Evd
@@ -1795,17 +1794,17 @@ let declare_an_instance n s args =
let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
-let anew_instance ~pstate atts binders (name,t) fields =
+let anew_instance atts binders (name,t) fields =
let program_mode = atts.program in
- let _id, pstate = new_instance ~pstate ~program_mode atts.polymorphic
+ let _id, proof = Classes.new_instance ~program_mode atts.polymorphic
name binders t (Some (true, CAst.make @@ CRecord (fields)))
~global:atts.global ~generalize:false Hints.empty_hint_info
in
- pstate
+ assert (Option.is_empty proof) (* refine:false with term *)
-let declare_instance_refl ~pstate atts binders a aeq n lemma =
+let declare_instance_refl atts binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
- in anew_instance ~pstate atts binders instance
+ in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "reflexivity"),lemma)]
let declare_instance_sym atts binders a aeq n lemma =
@@ -1818,41 +1817,41 @@ let declare_instance_trans atts binders a aeq n lemma =
in anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "transitivity"),lemma)]
-let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
+let declare_relation atts ?(binders=[]) a aeq n refl symm trans =
init_setoid ();
let instance = declare_instance a aeq (add_suffix n "_relation") "Coq.Classes.RelationClasses.RewriteRelation" in
- let pstate = anew_instance ~pstate atts binders instance [] in
+ let () = anew_instance atts binders instance [] in
match (refl,symm,trans) with
- (None, None, None) -> pstate
+ (None, None, None) -> ()
| (Some lemma1, None, None) ->
- declare_instance_refl ~pstate atts binders a aeq n lemma1
+ declare_instance_refl atts binders a aeq n lemma1
| (None, Some lemma2, None) ->
- declare_instance_sym ~pstate atts binders a aeq n lemma2
+ declare_instance_sym atts binders a aeq n lemma2
| (None, None, Some lemma3) ->
- declare_instance_trans ~pstate atts binders a aeq n lemma3
+ declare_instance_trans atts binders a aeq n lemma3
| (Some lemma1, Some lemma2, None) ->
- let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
- declare_instance_sym ~pstate atts binders a aeq n lemma2
+ let () = declare_instance_refl atts binders a aeq n lemma1 in
+ declare_instance_sym atts binders a aeq n lemma2
| (Some lemma1, None, Some lemma3) ->
- let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
- let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let () = declare_instance_refl atts binders a aeq n lemma1 in
+ let () = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in
- anew_instance ~pstate atts binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1);
(qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]
| (None, Some lemma2, Some lemma3) ->
- let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
- let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let () = declare_instance_sym atts binders a aeq n lemma2 in
+ let () = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in
- anew_instance ~pstate atts binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2);
(qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]
| (Some lemma1, Some lemma2, Some lemma3) ->
- let pstate = declare_instance_refl ~pstate atts binders a aeq n lemma1 in
- let pstate = declare_instance_sym ~pstate atts binders a aeq n lemma2 in
- let pstate = declare_instance_trans ~pstate atts binders a aeq n lemma3 in
+ let () = declare_instance_refl atts binders a aeq n lemma1 in
+ let () = declare_instance_sym atts binders a aeq n lemma2 in
+ let () = declare_instance_trans atts binders a aeq n lemma3 in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in
- anew_instance ~pstate atts binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]
@@ -1951,15 +1950,15 @@ let warn_add_setoid_deprecated =
CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
Pp.(str "Add Setoid is deprecated, please use Add Parametric Relation."))
-let add_setoid ~pstate atts binders a aeq t n =
+let add_setoid atts binders a aeq t n =
warn_add_setoid_deprecated ?loc:a.CAst.loc ();
init_setoid ();
- let pstate = declare_instance_refl ~pstate atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
- let pstate = declare_instance_sym ~pstate atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
- let pstate = declare_instance_trans ~pstate atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
+ let () = declare_instance_refl atts binders a aeq n (mkappc "Seq_refl" [a;aeq;t]) in
+ let () = declare_instance_sym atts binders a aeq n (mkappc "Seq_sym" [a;aeq;t]) in
+ let () = declare_instance_trans atts binders a aeq n (mkappc "Seq_trans" [a;aeq;t]) in
let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence"
in
- anew_instance ~pstate atts binders instance
+ anew_instance atts binders instance
[(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]);
(qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]
@@ -1988,7 +1987,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
(None,(instance,uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
- add_instance (Classes.mk_instance
+ Classes.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);
None
@@ -1999,7 +1998,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
let hook _ _ _ = function
| Globnames.ConstRef cst ->
- add_instance (Classes.mk_instance
+ Classes.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)
@@ -2011,7 +2010,7 @@ let add_morphism_infer atts m n : Proof_global.pstate option =
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 =
+let add_morphism atts binders m s n =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let instance_name = (CAst.make @@ Name instance_id),None in
@@ -2021,12 +2020,12 @@ let add_morphism ~pstate atts binders m s n =
[cHole; s; m])
in
let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
- let _, pstate = new_instance ~pstate
+ let _, pstate = Classes.new_instance
~program_mode:atts.program ~global:atts.global atts.polymorphic
instance_name binders instance_t None
~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
in
- pstate
+ Option.get pstate (* no instance body -> always open proof *)
(** Bind to "rewrite" too *)
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index cab7d0065e..e1cbc46b3b 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -81,18 +81,35 @@ val cl_rewrite_clause :
val is_applied_rewrite_relation :
env -> evar_map -> rel_context -> constr -> types option
-val declare_relation : pstate:Proof_global.t option -> rewrite_attributes ->
- ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t ->
- constr_expr option -> constr_expr option -> constr_expr option -> Proof_global.t option
-
-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 declare_relation
+ : rewrite_attributes
+ -> ?binders:local_binder_expr list
+ -> constr_expr
+ -> constr_expr
+ -> Id.t
+ -> constr_expr option
+ -> constr_expr option
+ -> constr_expr option
+ -> unit
+
+val add_setoid
+ : rewrite_attributes
+ -> local_binder_expr list
+ -> constr_expr
+ -> constr_expr
+ -> constr_expr
+ -> Id.t
+ -> unit
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
+val add_morphism
+ : rewrite_attributes
+ -> local_binder_expr list
+ -> constr_expr
+ -> constr_expr
+ -> Id.t
+ -> Proof_global.pstate
val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index 49c547a979..bd1f925486 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -90,7 +90,6 @@ let tac2def_typ = Entry.create "tactic:tac2def_typ"
let tac2def_ext = Entry.create "tactic:tac2def_ext"
let tac2def_syn = Entry.create "tactic:tac2def_syn"
let tac2def_mut = Entry.create "tactic:tac2def_mut"
-let tac2def_run = Entry.create "tactic:tac2def_run"
let tac2mode = Entry.create "vernac:ltac2_command"
let ltac1_expr = Pltac.tactic_expr
@@ -114,7 +113,7 @@ let pattern_of_qualid qid =
GRAMMAR EXTEND Gram
GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn
- tac2def_mut tac2def_run;
+ tac2def_mut;
tac2pat:
[ "1" LEFTA
[ qid = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> {
@@ -288,9 +287,6 @@ GRAMMAR EXTEND Gram
tac2def_mut:
[ [ "Set"; qid = Prim.qualid; ":="; e = tac2expr -> { StrMut (qid, e) } ] ]
;
- tac2def_run:
- [ [ "Eval"; e = tac2expr -> { StrRun e } ] ]
- ;
tac2typ_knd:
[ [ t = tac2type -> { CTydDef (Some t) }
| "["; ".."; "]" -> { CTydOpn }
@@ -878,20 +874,27 @@ PRINTED BY { pr_ltac2entry }
| [ tac2def_ext(e) ] -> { e }
| [ tac2def_syn(e) ] -> { e }
| [ tac2def_mut(e) ] -> { e }
-| [ tac2def_run(e) ] -> { e }
+END
+
+VERNAC ARGUMENT EXTEND ltac2_expr
+PRINTED BY { pr_ltac2expr }
+| [ tac2expr(e) ] -> { e }
END
{
let classify_ltac2 = function
| StrSyn _ -> Vernacextend.(VtSideff [], VtNow)
-| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ | StrRun _ -> Vernacextend.classify_as_sideeff
+| StrMut _ | StrVal _ | StrPrm _ | StrTyp _ -> Vernacextend.classify_as_sideeff
}
VERNAC COMMAND EXTEND VernacDeclareTactic2Definition
-| #[ local = locality ] ![proof] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
- fun ~pstate -> Tac2entries.register_struct ?local ~pstate:(Option.map Proof_global.get_current_pstate pstate) e; pstate
+| #[ local = locality ] [ "Ltac2" ltac2_entry(e) ] => { classify_ltac2 e } -> {
+ Tac2entries.register_struct ?local e
+ }
+| ![proof_opt_query] [ "Ltac2" "Eval" ltac2_expr(e) ] => { Vernacextend.classify_as_sideeff } -> {
+ fun ~pstate -> Tac2entries.perform_eval ~pstate e
}
END
@@ -899,15 +902,6 @@ END
let _ = Pvernac.register_proof_mode "Ltac2" tac2mode
-}
-
-VERNAC ARGUMENT EXTEND ltac2_expr
-PRINTED BY { pr_ltac2expr }
-| [ tac2expr(e) ] -> { e }
-END
-
-{
-
open G_ltac
open Vernacextend
@@ -917,9 +911,7 @@ VERNAC { tac2mode } EXTEND VernacLtac2
| ![proof] [ ltac2_expr(t) ltac_use_default(default) ] =>
{ classify_as_proofstep } -> {
(* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *)
- fun ~pstate ->
- Option.map (fun pstate -> Tac2entries.call ~pstate ~default t) pstate
- }
+ fun ~pstate -> Tac2entries.call ~pstate ~default t }
END
{
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 254c2e5086..246fe47c4a 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -769,13 +769,12 @@ let perform_eval ~pstate e =
(** Toplevel entries *)
-let register_struct ?local ~pstate str = match str with
+let register_struct ?local str = match str with
| StrVal (mut, isrec, e) -> register_ltac ?local ~mut isrec e
| StrTyp (isrec, t) -> register_type ?local isrec t
| StrPrm (id, t, ml) -> register_primitive ?local id t ml
| StrSyn (tok, lev, e) -> register_notation ?local tok lev e
| StrMut (qid, e) -> register_redefinition ?local qid e
-| StrRun e -> perform_eval ~pstate e
(** Toplevel exception *)
@@ -857,7 +856,7 @@ let print_ltac qid =
(** Calling tactics *)
let solve ~pstate default tac =
- let pstate, status = Proof_global.with_current_proof begin fun etac p ->
+ let pstate, status = Proof_global.with_proof begin fun etac p ->
let with_end_tac = if default then Some etac else None in
let g = Goal_select.get_default_goal_selector () in
let (p, status) = Pfedit.solve g None tac ?with_end_tac p in
diff --git a/user-contrib/Ltac2/tac2entries.mli b/user-contrib/Ltac2/tac2entries.mli
index e02c126e71..273cf02c9b 100644
--- a/user-contrib/Ltac2/tac2entries.mli
+++ b/user-contrib/Ltac2/tac2entries.mli
@@ -23,13 +23,14 @@ val register_primitive : ?local:bool ->
val register_struct
: ?local:bool
- -> pstate:Proof_global.pstate option
-> strexpr
-> unit
val register_notation : ?local:bool -> sexpr list -> int option ->
raw_tacexpr -> unit
+val perform_eval : pstate:Proof_global.pstate option -> raw_tacexpr -> unit
+
(** {5 Notations} *)
type scope_rule =
@@ -50,7 +51,7 @@ val print_ltac : Libnames.qualid -> unit
(** {5 Eval loop} *)
(** Evaluate a tactic expression in the current environment *)
-val call : pstate:Proof_global.t -> default:bool -> raw_tacexpr -> Proof_global.t
+val call : pstate:Proof_global.pstate -> default:bool -> raw_tacexpr -> Proof_global.pstate
(** {5 Toplevel exceptions} *)
diff --git a/user-contrib/Ltac2/tac2expr.mli b/user-contrib/Ltac2/tac2expr.mli
index 2e7dfc42db..af7bc32785 100644
--- a/user-contrib/Ltac2/tac2expr.mli
+++ b/user-contrib/Ltac2/tac2expr.mli
@@ -168,8 +168,6 @@ type strexpr =
(** Syntactic extensions *)
| StrMut of qualid * raw_tacexpr
(** Redefinition of mutable globals *)
-| StrRun of raw_tacexpr
- (** Toplevel evaluation of an expression *)
(** {5 Dynamic semantics} *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c783531f91..b9f57c0727 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -404,7 +404,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
| None ->
pstate
-let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
+let do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props =
let props =
match props with
| Some (true, { CAst.v = CRecord fs }) ->
@@ -487,17 +487,18 @@ let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode ct
if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
let term = to_constr sigma (Option.get term) in
(declare_instance_constant pri global imps ?hook id decl poly sigma term termtype;
- pstate)
+ None)
else if program_mode then
- (declare_instance_program env sigma ~global ~poly id pri imps decl term termtype ; pstate)
+ (declare_instance_program env sigma ~global ~poly id pri imps decl term termtype;
+ None)
else if Option.is_empty props then
- let pstate' =
+ let pstate =
Flags.silently (fun () ->
declare_instance_open sigma ?hook ~tac ~global ~poly
id pri imps decl (List.map RelDecl.get_name ctx) term termtype)
()
in
- Some (Proof_global.push ~ontop:pstate pstate')
+ Some pstate
else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in
id, pstate
@@ -529,7 +530,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl tclass
let sigma = resolve_typeclasses ~filter:Typeclasses.all_evars ~fail:true env sigma in
sigma, cl, u, c', ctx', ctx, imps, args, decl
-let new_instance ~pstate ?(global=false) ~program_mode
+let new_instance ?(global=false) ~program_mode
poly instid ctx cl props
?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
@@ -545,7 +546,7 @@ let new_instance ~pstate ?(global=false) ~program_mode
Namegen.next_global_ident_away i (Termops.vars_of_env env)
in
let env' = push_rel_context ctx env in
- do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode
+ do_instance env env' sigma ?hook ~tac ~global ~poly ~program_mode
cty k u ctx ctx' pri decl imps subst id props
let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index f80dbb9897..d441fd342c 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -32,8 +32,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
(** globality, reference, optional priority and pattern information *)
val new_instance :
- pstate:Proof_global.t option
- -> ?global:bool (** Not global by default. *)
+ ?global:bool (** Not global by default. *)
-> program_mode:bool
-> Decl_kinds.polymorphic
-> name_decl
@@ -44,7 +43,7 @@ val new_instance :
-> ?tac:unit Proofview.tactic
-> ?hook:(GlobRef.t -> unit)
-> Hints.hint_info_expr
- -> Id.t * Proof_global.t option (* May open a proof *)
+ -> Id.t * Proof_global.pstate option (* May open a proof *)
val declare_new_instance
: ?global:bool (** Not global by default. *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f92c1f9c27..34b5e13cd8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -60,6 +60,10 @@ let with_pstate ~pstate f =
vernac_require_open_proof ~pstate
(fun ~pstate -> f ~pstate:(Proof_global.get_current_pstate pstate))
+let modify_pstate ~pstate f =
+ vernac_require_open_proof ~pstate (fun ~pstate ->
+ Some (Proof_global.modify_current_pstate (fun pstate -> f ~pstate) pstate))
+
let get_current_or_global_context ~pstate =
match pstate with
| None -> let env = Global.env () in Evd.(from_env env, env)
@@ -1100,7 +1104,7 @@ let focus_command_cond = Proof.no_cond command_focus
all tactics fail if there are no further goals to prove. *)
let vernac_solve_existential ~pstate n com =
- Proof_global.simple_with_current_proof (fun _ p ->
+ Proof_global.modify_proof (fun p ->
let intern env sigma = Constrintern.intern_constr env sigma com in
Proof.V82.instantiate_evar (Global.env ()) n intern p) pstate
@@ -2441,7 +2445,8 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
(* Type classes *)
| VernacInstance (name, bl, t, props, info) ->
- snd @@ with_def_attributes ~atts (vernac_instance ~pstate name bl t props info)
+ with_maybe_open_proof ~pstate (fun ~pstate:_ ->
+ snd @@ with_def_attributes ~atts (vernac_instance name bl t props info))
| VernacDeclareInstance (id, bl, inst, info) ->
with_def_attributes ~atts vernac_declare_instance id bl inst info;
pstate
@@ -2459,7 +2464,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option =
(* Solving *)
| VernacSolveExistential (n,c) ->
unsupported_attributes atts;
- Some (vernac_require_open_proof ~pstate (vernac_solve_existential n c))
+ modify_pstate ~pstate (vernac_solve_existential n c)
(* Auxiliary file and library management *)
| VernacAddLoadPath (isrec,s,alias) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 12451370c8..5e6e9fdb0f 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -44,6 +44,10 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
(** Helper *)
val vernac_require_open_proof : pstate:Proof_global.t option -> (pstate:Proof_global.t -> 'a) -> 'a
+val with_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> 'a) -> 'a
+
+val modify_pstate : pstate:Proof_global.t option -> (pstate:Proof_global.pstate -> Proof_global.pstate) -> Proof_global.t option
+
(* Flag set when the test-suite is called. Its only effect to display
verbose information for `Fail` *)
val test_mode : bool ref
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 9ab2d00fc2..6eb618ad0a 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -34,6 +34,8 @@ type t = {
shallow : bool (* is the state trimmed down (libstack) *)
}
+let pstate st = Option.map Proof_global.get_current_pstate st.proof
+
let s_cache = ref None
let s_proof = ref None
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index dff81ad9bb..3d21b475e9 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -25,6 +25,8 @@ type t = {
shallow : bool (* is the state trimmed down (libstack) *)
}
+val pstate : t -> Proof_global.pstate option
+
val freeze_interp_state : marshallable:bool -> t
val unfreeze_interp_state : t -> unit
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:00:48 +0000