diff options
Diffstat (limited to 'coqpp/coqpp_main.ml')
| -rw-r--r-- | coqpp/coqpp_main.ml | 21 |
1 files changed, 20 insertions, 1 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) |