diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-29 18:31:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-30 02:20:15 +0100 |
| commit | 203b0eaac832af3b62e484c1aef89a02ffe8e29b (patch) | |
| tree | e7bd721dd8a0e0ad26567158ff5bfa3b68620c7c /intf/tacexpr.mli | |
| parent | a4cc4ea007b074009bea485e75f7efef3d4d25f3 (diff) | |
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.
Diffstat (limited to 'intf/tacexpr.mli')
| -rw-r--r-- | intf/tacexpr.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index aa1088c9e..6d10ef9d5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -292,9 +292,9 @@ and 'a gen_tactic_expr = | TacFun of 'a gen_tactic_fun_ast | TacArg of 'a gen_tactic_arg located (* For ML extensions *) - | TacML of Loc.t * ml_tactic_entry * 'l generic_argument list + | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'l generic_argument) list + | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list constraint 'a = < term:'t; |