Enrico Tassi

icon indicating a website link http://www-sop.inria.fr/members/Enrico.Tassi/

icon company @coq @math-comp @LPCIC icon location Inria Sophia-Antipolis icon location I'm a researcher in CS, mainly formal proofs and the implementation of proof assistants. I'm a hacker, a free software supporter

Results 963 comments of Enrico Tassi

Quoted terms do not use primitive projections

See https://github.com/LPCIC/coq-elpi/blob/master/Changelog.md#hoas-5 , this is intended (although maybe not decently documented next to the `primitive` symbol declaration in coq-builtin

`mixin-instance-type->mixin-src` does not use the typing information

Can you invoke coq.sigma.print between the two calls?

Bad interaction between `apply:` and typeclass solver

Would you be so nice to attach the output of Set Debug Typeclasses for the first run? I suspect it runs, solves it using hyp, but then we toss the...