diff options
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; |