diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/pfedit.ml | 5 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 6 | ||||
| -rw-r--r-- | proofs/proof.ml | 9 | ||||
| -rw-r--r-- | proofs/proof.mli | 3 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 16 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
6 files changed, 40 insertions, 3 deletions
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e67c595bd9..3d507f3583 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -91,6 +91,11 @@ let set_end_tac tac = let tac = Proofview.V82.tactic tac in Proof_global.set_endline_tactic tac +let set_used_variables l = + Proof_global.set_used_variables l +let get_used_variables () = + Proof_global.get_used_variables () + exception NoSuchGoal let _ = Errors.register_handler begin function | NoSuchGoal -> Util.error "No such goal." diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 289e8c13c1..7297b975f8 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -154,6 +154,12 @@ val get_all_proof_names : unit -> identifier list val set_end_tac : tactic -> unit (** {6 ... } *) +(** [set_used_variables l] declares that section variables [l] will be + used in the proof *) +val set_used_variables : identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + +(** {6 ... } *) (** [solve_nth n tac] applies tactic [tac] to the [n]th subgoal of the current focused proof or raises a UserError if no proof is focused or if there is no [n]th subgoal *) diff --git a/proofs/proof.ml b/proofs/proof.ml index 2aa31cd253..72730495d7 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -119,6 +119,7 @@ type proof_state = { type proof_info = { mutable endline_tactic : unit Proofview.tactic ; + mutable section_vars : Sign.section_context option; initial_conclusions : Term.types list } @@ -219,6 +220,11 @@ let _unfocus pr = pr.state <- { pr.state with proofview = Proofview.unfocus fc pr.state.proofview } +let set_used_variables l p = + p.info.section_vars <- Some l + +let get_used_variables p = p.info.section_vars + (*** Endline tactic ***) (* spiwack this is an information about the UI, it might be a good idea to move @@ -364,7 +370,8 @@ let start goals = undo_stack = [] ; transactions = [] ; info = { endline_tactic = Proofview.tclUNIT (); - initial_conclusions = List.map snd goals } + initial_conclusions = List.map snd goals; + section_vars = None } } in _focus end_of_stack (Obj.repr ()) 1 (List.length goals) pr; diff --git a/proofs/proof.mli b/proofs/proof.mli index d80ac79af2..12af18f408 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -129,6 +129,9 @@ val get_proof_info : proof -> Store.t val set_proof_info : Store.t -> proof -> unit +(* Sets the section variables assumed by the proof *) +val set_used_variables : Sign.section_context -> proof -> unit +val get_used_variables : proof -> Sign.section_context option (*** Endline tactic ***) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index e9af46ba9b..2745270a65 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -267,6 +267,16 @@ let set_endline_tactic tac = let p = give_me_the_proof () in Proof.set_endline_tactic tac p +let set_used_variables l = + let p = give_me_the_proof () in + let env = Global.env () in + let ids = List.fold_right Idset.add l Idset.empty in + let ctx = Environ.keep_hyps env ids in + Proof.set_used_variables ctx p + +let get_used_variables () = + Proof.get_used_variables (give_me_the_proof ()) + let with_end_tac tac = let p = give_me_the_proof () in Proof.with_end_tac p tac @@ -278,9 +288,11 @@ let close_proof () = let id = get_current_proof_name () in let p = give_me_the_proof () in let proofs_and_types = Proof.return p in + let section_vars = Proof.get_used_variables p in let entries = List.map - (fun (c,t) -> { Entries.const_entry_body = c ; - const_entry_type = Some t; + (fun (c,t) -> { Entries.const_entry_body = c; + const_entry_secctx = section_vars; + const_entry_type = Some t; const_entry_opaque = true }) proofs_and_types in diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 2f9f4a549d..ed6a60c71f 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -82,6 +82,10 @@ val run_tactic : unit Proofview.tactic -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) val set_endline_tactic : unit Proofview.tactic -> unit +(** Sets the section variables assumed by the proof *) +val set_used_variables : Names.identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + (** Appends the endline tactic of the current proof to a tactic. *) val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic |