Damien Pous

Hi, same problem for me, many incoming messages are not backed up. (outgoing messages are, incoming MMS are, but for incoming SMS, it looks like random: messages from the same...

Hi @MSoegtropIMC, (Reopening the issue here for the record, and to follow-up) I can do that, sure. Can you be more explicit about what I should do in the _CoqProject...

Hi again @MSoegtropIMC, I did reorganise the files as proposed above in the v1.7.8 release: now the three examples are in folder examples/ and use the "From RelationAlgebra Require Import...

(for the first point, some access to a function like Cairo.text_extents would be an alternative)

Any news on this front? HB.mixin breaks syntactically if I "Set Universe Polymorphism", and it says "Attribute universes.polymorphic is not supported" if I start the declaration with "#[universes(polymorphic=yes)]".

Hi @aa755, aac_congruence has been on my todo list since the beginning, but it requires a non-trivial effort (coding and certifying an algorithm for... computing congruence closure modulo AAC). I...

Indeed aac_normalise does not work in hypotheses so far (and revert cannot help due to the way it's implemented). Still, this feature should not be too difficult to implement. Meanwhile,...

Indeed, the ordering of uninterpreted subterms (here variables) is unspecified. It is fixed in each call to aac_normalise, but not persistent across various calls. A patch should be feasible, but...

I've pushed a patch proposal in branch canonical-ordering (based on v8.19) @aa755 can you try it out? Does it fit your needs? @palmskog what would be the best way to...

Thanks @palmskog ; would be great indeed if you could do the releasing/packaging ; I'll take care of porting to master. (I'll start now in a side branch of master)...