diff options
Diffstat (limited to 'intf')
| -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 aa1088c9ea..6d10ef9d51 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; |