diff options
Diffstat (limited to 'plugins/ltac/tacexpr.mli')
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 64da097de..2c36faeff 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -10,13 +10,14 @@ open Loc open Names open Constrexpr open Libnames -open Nametab open Genredexpr open Genarg open Pattern open Misctypes open Locus +type ltac_constant = KerName.t + type direction_flag = bool (* true = Left-to-right false = right-to-right *) type lazy_flag = | General (* returns all possible successes *) |