aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-07 23:59:08 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-08 16:55:46 +0200
commit52c3917be7239f7d5ab1ba882275b4571463f585 (patch)
tree9458b71b44b5b04f649a054ace210b8382934dd3
parent1654b3989041b25e3b642ffde12125344342a54b (diff)
Making Proof_global terminator generic in external tactics.
-rw-r--r--ltac/g_obligations.ml414
-rw-r--r--ltac/tacinterp.ml1
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml13
-rw-r--r--proofs/proof_global.mli5
-rw-r--r--toplevel/obligations.mli4
-rw-r--r--toplevel/vernacentries.ml5
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