Jean-Christophe Léchenet
Jean-Christophe Léchenet
I think I encountered a similar problem. Here is the code: ``` Require Import Arith List Lia. From Equations Require Import Equations. Import ListNotations. Inductive Subseq {A : Type} :...
Version 1.2.3 on Coq 8.12.
By the way, strangely, the opam package version "1.2 beta2" is considered older than the version "1.2 beta", but no sure that it can be modified now it has been...
This could be done in a different pass after lowering.
Actually, it has been decided that the pass must be optional, and disabled when we use the "strict mode".
(I was asked by Jasmin with a kind `PLEASE REPORT`)
Interestingly, on `master` the error is different: `linearisation error assign not a word` (but I am also asked to report it).
After discussing with Benjamin, the error is justified, but should be improved (the `PLEASE REPORT` should be removed).
Another example: ``` export fn main (reg u64 r) -> reg u64 { reg u64 res; reg bool b b2; b = r == 0; b2 = r == 1;...
Interestingly, the first program now passes correctly on latest main. Maybe the pass propagate_inline_variable fixed the problem. The second program still produces the error, though.