diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-07 23:59:08 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-08 16:55:46 +0200 |
commit | 52c3917be7239f7d5ab1ba882275b4571463f585 (patch) | |
tree | 9458b71b44b5b04f649a054ace210b8382934dd3 | |
parent | 1654b3989041b25e3b642ffde12125344342a54b (diff) |
Making Proof_global terminator generic in external tactics.
-rw-r--r-- | ltac/g_obligations.ml4 | 14 | ||||
-rw-r--r-- | ltac/tacinterp.ml | 1 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | proofs/proof_global.ml | 13 | ||||
-rw-r--r-- | proofs/proof_global.mli | 5 | ||||
-rw-r--r-- | toplevel/obligations.mli | 4 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 5 |
7 files changed, 29 insertions, 15 deletions
diff --git a/ltac/g_obligations.ml4 b/ltac/g_obligations.ml4 index 987b9d538..db8daf32d 100644 --- a/ltac/g_obligations.ml4 +++ b/ltac/g_obligations.ml4 @@ -30,6 +30,17 @@ let () = end in Obligations.default_tactic := tac +let with_tac f tac = + let env = { Genintern.genv = Global.env (); ltacvars = Names.Id.Set.empty } in + let tac = match tac with + | None -> None + | Some tac -> + let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in + let _, tac = Genintern.generic_intern env tac in + Some tac + in + f tac + (* We define new entries for programs, with the use of this module * Subtac. These entries are named Subtac.<foo> *) @@ -66,6 +77,9 @@ GEXTEND Gram open Obligations +let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac + let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 177867abd..9e502682b 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -1969,7 +1969,6 @@ let interp_tac_gen lfun avoid_ids debug t = end } let interp t = interp_tac_gen Id.Map.empty [] (get_debug()) t -let _ = Proof_global.set_interp_tac interp (* Used to hide interpretation for pretty-print, now just launch tactics *) (* [global] means that [t] should be internalized outside of goals. *) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 9b0200039..f2f4b11ed 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -124,7 +124,7 @@ val get_all_proof_names : unit -> Id.t list (** [set_end_tac tac] applies tactic [tac] to all subgoal generate by [solve] *) -val set_end_tac : Tacexpr.raw_tactic_expr -> unit +val set_end_tac : Genarg.glob_generic_argument -> unit (** {6 ... } *) (** [set_used_variables l] declares that section variables [l] will be diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index f3ca19a90..2956d623f 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -90,7 +90,7 @@ type closed_proof = proof_object * proof_terminator type pstate = { pid : Id.t; terminator : proof_terminator CEphemeron.key; - endline_tactic : Tacexpr.raw_tactic_expr option; + endline_tactic : Genarg.glob_generic_argument option; section_vars : Context.Named.t option; proof : Proof.proof; strength : Decl_kinds.goal_kind; @@ -148,9 +148,6 @@ let cur_pstate () = let give_me_the_proof () = (cur_pstate ()).proof let get_current_proof_name () = (cur_pstate ()).pid -let interp_tac = ref (fun _ -> assert false) -let set_interp_tac f = interp_tac := f - let with_current_proof f = match !pstates with | [] -> raise NoCurrentProof @@ -158,7 +155,13 @@ let with_current_proof f = let et = match p.endline_tactic with | None -> Proofview.tclUNIT () - | Some tac -> !interp_tac tac in + | Some tac -> + let open Geninterp in + let ist = { lfun = Id.Map.empty; extra = TacStore.empty } in + let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in + let tac = Geninterp.interp tag ist tac in + Ftactic.run tac (fun _ -> Proofview.tclUNIT ()) + in let (newpr,ret) = f et p.proof in let p = { p with proof = newpr } in pstates := p :: rest; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 86fc1deff..97a21cf22 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -134,10 +134,7 @@ val simple_with_current_proof : (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit (** Sets the tactic to be used when a tactic line is closed with [...] *) -val set_endline_tactic : Tacexpr.raw_tactic_expr -> unit -val set_interp_tac : - (Tacexpr.raw_tactic_expr -> unit Proofview.tactic) - -> unit +val set_endline_tactic : Genarg.glob_generic_argument -> unit (** Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it) + a list of diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 69d206961..80b689144 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -87,9 +87,9 @@ val add_mutual_definitions : fixpoint_kind -> unit val obligation : int * Names.Id.t option * Constrexpr.constr_expr option -> - Tacexpr.raw_tactic_expr option -> unit + Genarg.glob_generic_argument option -> unit -val next_obligation : Names.Id.t option -> Tacexpr.raw_tactic_expr option -> unit +val next_obligation : Names.Id.t option -> Genarg.glob_generic_argument option -> unit val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress (* Number of remaining obligations to be solved for this program *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c1142c7cb..eff4d15c0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -844,8 +844,9 @@ let focus_command_cond = Proof.no_cond command_focus let vernac_solve_existential = instantiate_nth_evar_com let vernac_set_end_tac tac = - (** FIXME *) - let tac = Genarg.out_gen (Genarg.rawwit Constrarg.wit_ltac) tac in + let open Genintern in + let env = { genv = Global.env (); ltacvars = Id.Set.empty } in + let _, tac = Genintern.generic_intern env tac in if not (refining ()) then error "Unknown command of the non proof-editing mode."; set_end_tac tac |