Compile without Stdlib #514
Conversation
|
@CohenCyril @gares CI "green" but this is dropping support for 8.18, 819 and 8.20. Fine to me since we got a recent release supporting all of those and 9.0.0 should come soon but we might want to wait before merging. |
I'm in favor of waiting a bit. |
proux01
force-pushed
the
no-stdlib
branch
2 times, most recently
from
b65130f to
56437fa
Compare
|
Apparently it wasn't that hard to keep compatibility with 8.18-8.20, so let's merge. |
| @@ -1,5 +1,5 @@ | |||
| From HB Require Import structures. | |||
| From Coq Require Import ssreflect ZArith. | |||
| From Corelib Require Import ssreflect BinNums IntDef. | |||
There was a problem hiding this comment.
@proux01 this header is not rewritten when I run make with coq 8.20, is it expected?
There was a problem hiding this comment.
I guess, my only objective was to keep the main build on Coq 8.20, maybe not all examples.
There was a problem hiding this comment.
Ok, I'll make a patch to make examples work too
There was a problem hiding this comment.
I forgot that the CI was not testing the examples :-/
2 participants
No description provided.