Julien Puydt
Julien Puydt
It's a matter of something like "git tag 20180705" then "git push --tags", so it's not that complicated...
Please? If you're abandoning the mod and I shouldn't package it, just tell me...
I don't care that much about the Coq Platform -- Debian is another distribution entirely. I'd rather package an official version than a patched-up one, so I'll wait. There are...
I have given some thought on coercions these last months after seeing how many of them I needed in some Coq mathematics I wrote. I even added a `count_explicit_coercions` make...
@proux01 I'm not sure where you answered to whom, but: - for the eq3 question, if m, n and x are in NN, ZZ and RR and the context is...
No, mathematically there isn't always such a common domain. But at any point in a text, you have the necessary information ready at hand to figure things out - that's...
@hendriktews I've been trying to get in touch with you - especially about the Debian packaging for proofgeneral... could you contact me? I'm jpuydt and a Debian developer so you...
I have no clue where `write_trace` comes from... the three lines can probably replaced with something like `List.map (fun card -> Yojson.Safe.to_channel stdout card) cards` ; but first cards needs...
(now that I think of it, `write_trace` is probably from trace.atd)
Here is a first draft ; some output is different so it breaks some tests, but it doesn't look insane: ``` --- elpi.orig/src/elpi_trace_elaborator.ml +++ elpi/src/elpi_trace_elaborator.ml @@ -664,6 +664,6 @@ let...