diff options
Diffstat (limited to 'intf/tacexpr.mli')
| -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 26ab4b666..08063cf2a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -167,7 +167,7 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr = (* For syntax extensions *) | TacAlias of Loc.t * string * - (Id.t * 'lev generic_argument) list * (dir_path * glob_tactic_expr) + (Id.t * 'lev generic_argument) list * (Dir_path.t * glob_tactic_expr) (** Possible arguments of a tactic definition *) |