From 203b0eaac832af3b62e484c1aef89a02ffe8e29b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Dec 2015 18:31:17 +0100 Subject: External tactics and notations now accept any tactic argument. This commit has deep consequences in term of tactic evaluation, as it allows to pass any tac_arg to ML and alias tactics rather than mere generic arguments. This makes the evaluation much more uniform, and in particular it removes the special evaluation function for notations. This last point may break some notations out there unluckily. I had to treat in an ad-hoc way the tactic(...) entry of tactic notations because it is actually not interpreted as a generic argument but rather as a proper tactic expression instead. There is for now no syntax to pass any tactic argument to a given ML or notation tactic, but this should come soon. Also fixes bug #3849 en passant. --- plugins/setoid_ring/newring.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index d596cf6fb8..88c8465b1b 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -137,8 +137,8 @@ let closed_term_ast l = let l = List.map (fun gr -> ArgArg(Loc.ghost,gr)) l in TacFun([Some(Id.of_string"t")], TacML(Loc.ghost,tacname, - [Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None); - Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l])) + [TacGeneric (Genarg.in_gen (Genarg.glbwit Constrarg.wit_constr) (GVar(Loc.ghost,Id.of_string"t"),None)); + TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Constrarg.wit_ref)) l)])) (* let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term" *) @@ -228,7 +228,7 @@ let exec_tactic env evd n f args = (** Build the getter *) let lid = List.init n (fun i -> Id.of_string("x"^string_of_int i)) in let n = Genarg.in_gen (Genarg.glbwit Stdarg.wit_int) n in - let get_res = TacML (Loc.ghost, get_res, [n]) in + let get_res = TacML (Loc.ghost, get_res, [TacGeneric n]) in let getter = Tacexp (TacFun (List.map (fun id -> Some id) lid, get_res)) in (** Evaluate the whole result *) let gl = dummy_goal env evd in -- cgit v1.2.3