diff options
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 70ccfc139d..27663a0681 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -104,9 +104,10 @@ type instance_flag = bool option type export_flag = bool (* true = Export; false = Import *) +type one_import_filter_name = qualid * bool (* import inductive components *) type import_filter_expr = | ImportAll - | ImportNames of qualid list + | ImportNames of one_import_filter_name list type onlyparsing_flag = { onlyparsing : bool } (* Some v = Parse only; None = Print also. |