coqbot

Comment author: @silene Here is a reduced testcase. The anomaly is raised on 8.4 too. ```coq Definition ptrn : Set := unit -> (unit -> unit) -> (unit -> unit)...

Comment author: @JasonGross Created attachment 417 An example setup containing a run.sh file, which shows the problem Currently [Scheme] does not register its schemes with the database used by [find_scheme]...

Comment author: @zeldovich With a recent version of Coq from the v8.5 branch, the following program demonstrates a case where [setoid_rewrite] fails but [rewrite] succeeds. Require Import List. Goal (forall...

Comment author: @ppedrot Setoid rewrite is very different from rewrite, and does not use the same algorithm at all. Here, it fails to go under a case analysis because it...

Comment author: @zeldovich The behavior under 8.4 was the same.

Comment author: @ichung Compiling a Coq source file containing the command [Cd "some_dir".] incorrectly causes the resulting .vo file to be output to the "some_dir" directory. This compilation step should...

Comment author: @maximedenes This is used as a feature by some developments like Compcert. I'm not sure I buy the security argument, since compiling a .v file can already load...

Comment author: @jwiegley I have not narrowed this down to a smaller case. The project is: https://github.com/jwiegley/linearscan The commit where things go badly is 3cab019a6d882671bb8b22ea68405052653b55cb. Prior to this commit, I...

Comment author: @mattam82 Where's the linearScan function ?

Comment author: @jwiegley It's in Allocate.v, if you've checked out that commit.