{"action":"created","issue":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/801","repository_url":"https://api.github.com/repos/HoTT/HoTT","labels_url":"https://api.github.com/repos/HoTT/HoTT/issues/801/labels{/name}","comments_url":"https://api.github.com/repos/HoTT/HoTT/issues/801/comments","events_url":"https://api.github.com/repos/HoTT/HoTT/issues/801/events","html_url":"https://github.com/HoTT/HoTT/issues/801","id":149999937,"number":801,"title":"Anomaly when one uses Record synonyms in Context.","user":{"login":"georgydunaev","id":3389017,"avatar_url":"https://avatars.githubusercontent.com/u/3389017?v=3","gravatar_id":"","url":"https://api.github.com/users/georgydunaev","html_url":"https://github.com/georgydunaev","followers_url":"https://api.github.com/users/georgydunaev/followers","following_url":"https://api.github.com/users/georgydunaev/following{/other_user}","gists_url":"https://api.github.com/users/georgydunaev/gists{/gist_id}","starred_url":"https://api.github.com/users/georgydunaev/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/georgydunaev/subscriptions","organizations_url":"https://api.github.com/users/georgydunaev/orgs","repos_url":"https://api.github.com/users/georgydunaev/repos","events_url":"https://api.github.com/users/georgydunaev/events{/privacy}","received_events_url":"https://api.github.com/users/georgydunaev/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2016-04-21T08:15:33Z","updated_at":"2016-04-21T09:58:26Z","closed_at":null,"body":"I tried to reproduce this bug in standart coq, but I didn't have a success.\r\n_Anomaly: Uncaught exception Type_errors.TypeError( _, _). Please report._\r\nAll lines are essential.\r\n```\r\nRequire Import HoTT.\r\nRequire HoTT.categories.\r\nRequire Import Category.Core Category.Morphisms.\r\nRequire Import HoTT.categories.SimplicialSets.\r\n\r\nSection my.\r\nContext `{Funext}.\r\nDefinition sset := simplicial_set.\r\nContext (A B:simplicial_set).\r\nContext (f:morphism sset A B).\r\nTheorem anomaly:PreCategory.  \r\n```"},"comment":{"url":"https://api.github.com/repos/HoTT/HoTT/issues/comments/212839880","html_url":"https://github.com/HoTT/HoTT/issues/801#issuecomment-212839880","issue_url":"https://api.github.com/repos/HoTT/HoTT/issues/801","id":212839880,"user":{"login":"georgydunaev","id":3389017,"avatar_url":"https://avatars.githubusercontent.com/u/3389017?v=3","gravatar_id":"","url":"https://api.github.com/users/georgydunaev","html_url":"https://github.com/georgydunaev","followers_url":"https://api.github.com/users/georgydunaev/followers","following_url":"https://api.github.com/users/georgydunaev/following{/other_user}","gists_url":"https://api.github.com/users/georgydunaev/gists{/gist_id}","starred_url":"https://api.github.com/users/georgydunaev/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/georgydunaev/subscriptions","organizations_url":"https://api.github.com/users/georgydunaev/orgs","repos_url":"https://api.github.com/users/georgydunaev/repos","events_url":"https://api.github.com/users/georgydunaev/events{/privacy}","received_events_url":"https://api.github.com/users/georgydunaev/received_events","type":"User","site_admin":false},"created_at":"2016-04-21T09:58:26Z","updated_at":"2016-04-21T09:58:26Z","body":"I've isolated bug from HoTT.\r\n\r\nRecord qq:={\r\n obj : Type\r\n}.\r\nSection my. (*anomaly depends on this line*)\r\nContext (ww:qq).\r\nDefinition ss := ww .\r\nContext (A: obj ss).\r\nTheorem anomaly:nat.\r\n\r\nI you have no such bug, maybe I should reinstall the system. (it was last installed 3 weeks ago)\r\n\r\n(reported https://coq.inria.fr/bugs/show_bug.cgi?id=4686)"}}