diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.mli | 2 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 3 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 5 |
3 files changed, 6 insertions, 4 deletions
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 31e3d506b8..b527eb3245 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -117,7 +117,7 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be used in the proof *) -val set_used_variables : Id.t list -> unit +val set_used_variables : Id.t list -> Context.section_context val get_used_variables : unit -> Context.section_context option (** {6 ... } *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index dd0e146497..07ff6e41ad 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -259,7 +259,8 @@ let set_used_variables l = | p :: rest -> if not (Option.is_empty p.section_vars) then Errors.error "Used section variables can be declared only once"; - pstates := { p with section_vars = Some ctx} :: rest + pstates := { p with section_vars = Some ctx} :: rest; + ctx let get_open_goals () = let gl, gll, shelf , _ , _ = Proof.proof (cur_pstate ()).proof in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index c2c447c92c..c9a812c4ce 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,9 @@ val set_interp_tac : (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) -> unit -(** Sets the section variables assumed by the proof *) -val set_used_variables : Names.Id.t list -> unit +(** Sets the section variables assumed by the proof, returns its closure + * (w.r.t. type dependencies *) +val set_used_variables : Names.Id.t list -> Context.section_context val get_used_variables : unit -> Context.section_context option (**********************************************************) |