{"action":"created","issue":{"url":"https://api.github.com/repos/math-comp/math-comp/issues/75","repository_url":"https://api.github.com/repos/math-comp/math-comp","labels_url":"https://api.github.com/repos/math-comp/math-comp/issues/75/labels{/name}","comments_url":"https://api.github.com/repos/math-comp/math-comp/issues/75/comments","events_url":"https://api.github.com/repos/math-comp/math-comp/issues/75/events","html_url":"https://github.com/math-comp/math-comp/issues/75","id":182482443,"number":75,"title":"Compilation fails with current Coq 8.6 branch","user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars.githubusercontent.com/u/330628?v=3","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":2,"created_at":"2016-10-12T09:51:06Z","updated_at":"2016-10-12T16:22:02Z","closed_at":null,"body":"I am getting the following error when compiling ssreflect master (b0c734bcd978459e323c42acbde6c4a6d0f8b566) against Coq v8.6 (96ed527472c38e92727d8fb6bfc41770c43b762b):\r\n\r\n```\r\n$ nice make -j5\r\nGenerating Makefile.coq for Coq v8.6 with COQBIN=/home/r/bin/coq-8.6/bin/\r\n# Override COQDEP to find only the \"right\" copy .ml files\r\nCOQDEP ssreflect_plugin.mlpack\r\nCAMLDEP -pp ssreflect.ml4\r\nRedundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].\r\nCOQDEP tuple.v\r\nCOQDEP prime.v\r\nCOQDEP path.v\r\nCOQDEP generic_quotient.v\r\nCOQDEP fintype.v\r\nCOQDEP finset.v\r\nCOQDEP fingraph.v\r\nCOQDEP finfun.v\r\nCOQDEP div.v\r\nCOQDEP choice.v\r\nCOQDEP binomial.v\r\nCOQDEP bigop.v\r\nCOQDEP ssrnat.v\r\nCOQDEP ssrfun.v\r\nCOQDEP ssreflect.v\r\nCOQDEP ssrbool.v\r\nCOQDEP seq.v\r\nCOQDEP eqtype.v\r\nCOQDEP all_ssreflect.v\r\nCAMLC -pp -c ssreflect.ml4\r\nRedundant [TYPED AS] clause in [ARGUMENT EXTEND ssrindex].\r\nFile \"ssreflect.ml4\", line 675, characters 55-68:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 755, characters 25-37:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 756, characters 19-31:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 756, characters 33-45:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 757, characters 5-44:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 1252, characters 10-24:\r\nWarning 3: deprecated: Util.String.set\r\nUse Bytes.set instead.\r\nFile \"ssreflect.ml4\", line 4441, characters 26-123:\r\nWarning 40: this record of type Proofview.Goal.enter contains fields that are \r\nnot visible in the current scope: enter.\r\nThey will not be selected if the type becomes unknown.\r\nFile \"ssreflect.ml4\", line 1049, characters 6-9:\r\nWarning 26: unused variable fmt.\r\nFile \"ssreflect.ml4\", line 1053, characters 6-13:\r\nWarning 26: unused variable tacname.\r\nCAMLC -pack -o ssreflect_plugin.cmo\r\nmake[1]: *** No rule to make target 'ssreflect_plugin.mllib', needed by 'ssreflect_plugin.cmxa'.  Stop.\r\nMakefile:24: recipe for target 'all' failed\r\nmake: *** [all] Error 2\r\n```"},"comment":{"url":"https://api.github.com/repos/math-comp/math-comp/issues/comments/253262868","html_url":"https://github.com/math-comp/math-comp/issues/75#issuecomment-253262868","issue_url":"https://api.github.com/repos/math-comp/math-comp/issues/75","id":253262868,"user":{"login":"RalfJung","id":330628,"avatar_url":"https://avatars.githubusercontent.com/u/330628?v=3","gravatar_id":"","url":"https://api.github.com/users/RalfJung","html_url":"https://github.com/RalfJung","followers_url":"https://api.github.com/users/RalfJung/followers","following_url":"https://api.github.com/users/RalfJung/following{/other_user}","gists_url":"https://api.github.com/users/RalfJung/gists{/gist_id}","starred_url":"https://api.github.com/users/RalfJung/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/RalfJung/subscriptions","organizations_url":"https://api.github.com/users/RalfJung/orgs","repos_url":"https://api.github.com/users/RalfJung/repos","events_url":"https://api.github.com/users/RalfJung/events{/privacy}","received_events_url":"https://api.github.com/users/RalfJung/received_events","type":"User","site_admin":false},"created_at":"2016-10-12T16:22:02Z","updated_at":"2016-10-12T16:22:02Z","body":"Yes, I did the `git clean -xfd`. I also tried sequential building, to no avail."}}
{"actor":{"display_login":"RalfJung"}}