Process completed with exit code 1.

Syntax error: [univ_level_or_quality] or '|' or '}' expected (in [univ_annot]). Command exited with non-zero status 1

Syntax error: [univ_level_or_quality] or '|' or '}' expected (in [univ_annot]). Command exited with non-zero status 1

Unexpected input(s) 'name', 'authToken', 'extraPullNames', valid inputs are ['extra_nix_config', 'github_access_token', 'install_url', 'install_options', 'nix_path']

Could not find a terminator for warning: File "./theories/Basics/Overture.v", line 73, characters 0-8: Warning: Use of "Notation" keyword for abbreviations is deprecated, use "Abbreviation" instead. [notation-for-abbreviation,deprecated-since-9.2,deprecated,default]

There is no flag or option with this name: "Loose Hint Behavior".

"coq-core" has been renamed to "rocq-runtime".

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-90: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 10, characters 0-90: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "number_string_notation_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]

"coq-core" has been renamed to "rocq-runtime".

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 8, characters 0-54: Warning: "coq-core" has been renamed to "rocq-runtime". [coq-core-plugin,deprecated-since-9.0,deprecated,default]

Could not find a terminator for warning: File "./theories/Basics/Settings.v", line 8, characters 0-54: Warning: Legacy loading plugin method has been removed from Rocq, and the `:` syntax is deprecated, and its first argument ignored; please remove "ltac_plugin:" from your Declare ML [legacy-loading-removed,deprecated-since-9.0,deprecated,default]

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

Implicitly declaring hint databases is deprecated. Please explicitly

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

There is no flag or option with this name: "Loose Hint Behavior".

"coq-core" has been renamed to "rocq-runtime".