diff options
Diffstat (limited to 'vernac/vernacentries.ml')
| -rw-r--r-- | vernac/vernacentries.ml | 11 |
1 files changed, 8 insertions, 3 deletions
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) -> |