diff options
| author | Pierre-Marie Pédrot | 2015-12-31 13:56:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-01-02 02:02:02 +0100 |
| commit | f3e611b2115b425f875e971ac9ff7534c2af2800 (patch) | |
| tree | d153ca5e2205efe2ea76f5bdf05d967df80c3736 /intf | |
| parent | d5b1807e65f7ea29d435c3f894aa551370c5989f (diff) | |
Separation of concern in TacAlias API.
The TacAlias node now only contains the arguments fed to the tactic notation.
The binding variables are worn by the tactic representation in Tacenv.
Diffstat (limited to 'intf')
| -rw-r--r-- | intf/tacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 6d10ef9d51..05e7ea1a3b 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -294,7 +294,7 @@ and 'a gen_tactic_expr = (* For ML extensions *) | TacML of Loc.t * ml_tactic_entry * 'a gen_tactic_arg list (* For syntax extensions *) - | TacAlias of Loc.t * KerName.t * (Id.t * 'a gen_tactic_arg) list + | TacAlias of Loc.t * KerName.t * 'a gen_tactic_arg list constraint 'a = < term:'t; |