diff options
Diffstat (limited to 'plugins/ltac/tacexpr.mli')
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 3baa475ab..37abfeee9 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -36,6 +36,7 @@ type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) type goal_selector = Vernacexpr.goal_selector = + | SelectAlreadyFocused | SelectNth of int | SelectList of (int * int) list | SelectId of Id.t |