coqbot
coqbot
Comment author: @herbelin > I don't really know why the internal representation of patterns is done that > way, but it leads to the computation of a huge term. This...
Comment author: @ppedrot (In reply to Hugo Herbelin from comment [BZ#11](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%2311%22)) > If I understand your point clearly, you are taking about the internal types > of the pattern variables...
Comment author: @herbelin I suspect that Maxime would say that terms are up to reduction and that no inconsistency can be derived from choosing a different representative in a class...
Comment author: @maximedenes (In reply to Hugo Herbelin from comment [BZ#13](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%2313%22)) > I suspect that Maxime would say that terms are up to reduction and that no > inconsistency can...
Comment author: @mattam82 Changing the structure of match to not include the types of the patterns could be a costly operation implementation-wise and performance-wise I think, as you need type...
Comment author: @herbelin (In reply to Matthieu Sozeau from comment [BZ#15](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%2315%22)) > Changing the structure of match to not include the types of the patterns > could be a costly...
Comment author: @ppedrot An alternative solution that may actually be more efficient in general would be to restrict the kernel reduction so that it never reduces the types of patterns....
Comment author: @herbelin (In reply to Pierre-Marie Pédrot from comment [BZ#17](https://github.com/coq/coq/issues?q=is%3Aissue%20%22Original%20bug%20ID%3A%20BZ%2317%22)) > An alternative solution that may actually be more efficient in general would > be to restrict the kernel...
Comment author: @silene Perhaps I am missing something, but I don't think it would work to not perform reduction in the pattern types. It is not a matter of consistency...
Comment author: @tchajed The following code triggers a subst bug: ```coq (* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Fscq" "-top" "Mem") -*- *) (* File reduced by coq-bug-finder from...