diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 0fd4130d24..bdc8f3367c 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -165,7 +165,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacExtend of loc * string * ('constr,'tac) generic_argument list (* For syntax extensions *) - | TacAlias of string * + | TacAlias of loc * string * (identifier * ('constr,'tac) generic_argument) list * 'tac |