diff options
| author | Enrico Tassi | 2021-01-06 17:31:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2021-01-27 09:45:49 +0100 |
| commit | 0a531fae53c31ef76ff25fbfd3ceb8b5b33aa264 (patch) | |
| tree | d528c369ca7797a746666977258482f7e32c7b5f /sysinit/coqargs.mli | |
| parent | 2caae4d530ba97ced98711986dc504f9becdab81 (diff) | |
[coqargs] use standard option injection for -type-in-type
Diffstat (limited to 'sysinit/coqargs.mli')
| -rw-r--r-- | sysinit/coqargs.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/sysinit/coqargs.mli b/sysinit/coqargs.mli index acf941f730..cc622fabe3 100644 --- a/sysinit/coqargs.mli +++ b/sysinit/coqargs.mli @@ -33,6 +33,7 @@ type injection_command = type coqargs_logic_config = { impredicative_set : Declarations.set_predicativity; indices_matter : bool; + type_in_type : bool; toplevel_name : top; } |