Wrong evaluation order with sequential modifier

[NotBad4U]

Hi everyone!

When the modifier sequential is used on a symbol, the order of execution is reversed.
The last case is evaluated first ("toto (⊤ ∧ ⊤) ↪ ⊥" in the below example).

sequential symbol toto: Prop →  Prop;
rule toto (⊤ ∧ ⊤) ↪ ⊤
with toto (⊤ ∧ ⊤) ↪ ⊥;

compute toto (⊤ ∧ ⊤);   // compute ⊥ 

[fblanqui]

Hi @gabrielhdt . This is for you I think. ;-) I guess there is a list to reverse somewhere...