Updating to rocq9.2/mathcomp2.6 - #61
Conversation
| - case: eqP U1=>// <-; move: (consec_mem C). | ||
| by rewrite inE (negbTE Nt1k) /= =>->. | ||
| (* then the proof is straightforward *) | ||
| (* then the proof is straightforewriteard *) |
| (* induction over union maps, expressed with pts and \+ *) | ||
|
|
||
| (* forward progressing over keys *) | ||
| (* forewriteard progressing over keys *) |
There was a problem hiding this comment.
i just fixed those, will commit soon. but how to fix the dependency? CI says it can't find coq >= 9.2. I guess it wants rocq. Should I just change it by hand in meta-yaml?
|
@clayrat Hm, how to fix the ci for 9.2? |
|
@clayrat @palmskog Hi guys. I'm having trouble with getting docker to accept to test fcsl-pcm against the docker image mathcomp:2.6.0-rocq-prover-9.2. I'm getting some cryptic error message that it can't satisfy the dependency for coq >= 9.2, and I'm not sure how to make it satisfy it. Any help appreciated. |
|
@aleksnanevski I guess we both fixed it in parallel. The underlying cause is rocq-community/templates#142, i.e. the fact that templates that we use for |
|
Yes, thanks for this. I'm doing some minor fixes now, and plan to make a new release in a few minutes. |
2 participants
No description provided.