diff options
author | 2016-09-16 13:54:13 +0200 | |
---|---|---|
committer | 2016-09-16 13:54:13 +0200 | |
commit | 978dd21af8467aa483bce551b3d5df8895cfff0f (patch) | |
tree | 41f473bddf855d3daf179c83ed63166834ae3240 /proofs | |
parent | 89f7bc53fbd558e3b5ff2ce1d1693f570afcc536 (diff) | |
parent | 7bd00a63015c4017d8209a4d495b9683d33d1d53 (diff) |
Make the Coq codebase independent from Ltac-related code.
We untangle many dependencies on Ltac datastructures and modules from the
lower strata, resulting in a self-contained ltac/ folder. While not a plugin
yet, the change is now very easy to perform. The main API changes have been
documented in the dev/doc/changes file.
The patches are quite rough, and it may be the case that some parts of the
code can migrate back from ltac/ to a core folder. This should be decided on
a case-by-case basis, according to a more long-term consideration of what is
exactly Ltac-dependent and whatnot.
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
-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-- | proofs/proof_type.mli | 1 |
5 files changed, 11 insertions, 12 deletions
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli index aa091aecd..8a096b645 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.mli @@ -10,8 +10,8 @@ open Term open Clenv -open Tacexpr open Unification +open Misctypes (** Tactics *) val unify : ?flags:unify_flags -> constr -> unit Proofview.tactic 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/proofs/proof_type.mli b/proofs/proof_type.mli index f7798a0ed..ff60ae5bf 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -11,7 +11,6 @@ open Evd open Names open Term -open Tacexpr open Glob_term open Nametab open Misctypes |