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.

1 files changed, 3 insertions, 3 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 08d2d21a3f..93d64f686d 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -656,11 +656,11 @@ and intern_tactic_seq onlytac ist = function
 
   (* For extensions *)
   | TacAlias (loc,s,l) ->
-      let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
+      let l = List.map (fun (id,a) -> (id,intern_tacarg !strict_check false ist a)) l in
       ist.ltacvars, TacAlias (loc,s,l)
   | TacML (loc,opn,l) ->
       let _ignore = Tacenv.interp_ml_tactic opn in
-      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
+      ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_tacarg !strict_check false ist) l)
 
 and intern_tactic_as_arg loc onlytac ist a =
   match intern_tacarg !strict_check onlytac ist a with
@@ -700,7 +700,7 @@ and intern_tacarg strict onlytac ist = function
   | TacNumgoals -> TacNumgoals
   | Tacexp t -> Tacexp (intern_tactic onlytac ist t)
   | TacGeneric arg ->
-    let (_, arg) = Genintern.generic_intern ist arg in
+    let arg = intern_genarg ist arg in
     TacGeneric arg
 
 (* Reads the rules of a Match Context or a Match *)