diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/classes.ml | 15 | ||||
| -rw-r--r-- | vernac/classes.mli | 5 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 11 | ||||
| -rw-r--r-- | vernac/vernacentries.mli | 4 | ||||
| -rw-r--r-- | vernac/vernacstate.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 2 |
6 files changed, 26 insertions, 13 deletions
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 |