Skip to content
Snippets Groups Projects
Commit 9fd57032 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.

parent f8d00956
No related branches found
No related tags found
1 merge request!419Use `-native-compiler no` to make sure we do not rely on (bugs) in `native_compute`.
Pipeline #73622 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
_CoqProject
+ 1
− 0
View file @ 9fd57032
...@@ -2,6 +2,7 @@ ...@@ -2,6 +2,7 @@
# `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package. # `-Q $PACKAGE[/ ]` so that we can filter out the right ones for each package.
-Q stdpp stdpp -Q stdpp stdpp
-Q stdpp_unstable stdpp.unstable -Q stdpp_unstable stdpp.unstable
-arg -native-compiler -arg no
# 'Global Hint Rewrite' not supported before Coq 8.14. # 'Global Hint Rewrite' not supported before Coq 8.14.
-arg -w -arg -deprecated-hint-rewrite-without-locality -arg -w -arg -deprecated-hint-rewrite-without-locality
# Fixing this one requires Coq 8.15. # Fixing this one requires Coq 8.15.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment