diff options
Diffstat (limited to 'tactics/tacintern.ml')
| -rw-r--r-- | tactics/tacintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 883b9094f2..dc84fa5922 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -52,7 +52,7 @@ let skip_metaid = function (** Generic arguments *) -type glob_sign = { +type glob_sign = Genarg.glob_sign = { ltacvars : Id.t list * Id.t list; (* ltac variables and the subset of vars introduced by Intro/Let/... *) ltacrecvars : (Id.t * ltac_constant) list; |