{"action":"created","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/129","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/129/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/129/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/129/events","html_url":"https://github.com/UniMath/UniMath/issues/129","id":100638150,"number":129,"title":"UniMath/Foundations/Generalities/uu0a.v: pretty-printing of ~","user":{"login":"nyraghu","id":11349287,"avatar_url":"https://avatars.githubusercontent.com/u/11349287?v=3","gravatar_id":"","url":"https://api.github.com/users/nyraghu","html_url":"https://github.com/nyraghu","followers_url":"https://api.github.com/users/nyraghu/followers","following_url":"https://api.github.com/users/nyraghu/following{/other_user}","gists_url":"https://api.github.com/users/nyraghu/gists{/gist_id}","starred_url":"https://api.github.com/users/nyraghu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/nyraghu/subscriptions","organizations_url":"https://api.github.com/users/nyraghu/orgs","repos_url":"https://api.github.com/users/nyraghu/repos","events_url":"https://api.github.com/users/nyraghu/events{/privacy}","received_events_url":"https://api.github.com/users/nyraghu/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":14,"created_at":"2015-08-12T21:19:25Z","updated_at":"2015-08-25T09:07:14Z","closed_at":"2015-08-25T09:07:14Z","body":"Coqdoc wrongly pretty-prints the homotopy infix operator ~ as the negation symbol ¬ in the HTML documentation created by \"make doc\".  [Section 15.4.1 of the Coq manual](https://coq.inria.fr/distrib/V8.5beta2/refman/Reference-Manual017.html#coqdoc) says that this translation is specified by the current pretty-printing table.  To correct it, it appears that one has to write\r\n\r\n(** printing ~ #~# *)\r\n\r\nor perhaps\r\n\r\n(** remove printing ~ *)\r\n\r\nin each file that uses the ~ notation."},"comment":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/comments/134534540","html_url":"https://github.com/UniMath/UniMath/issues/129#issuecomment-134534540","issue_url":"https://api.github.com/repos/UniMath/UniMath/issues/129","id":134534540,"user":{"login":"benediktahrens","id":1106102,"avatar_url":"https://avatars.githubusercontent.com/u/1106102?v=3","gravatar_id":"","url":"https://api.github.com/users/benediktahrens","html_url":"https://github.com/benediktahrens","followers_url":"https://api.github.com/users/benediktahrens/followers","following_url":"https://api.github.com/users/benediktahrens/following{/other_user}","gists_url":"https://api.github.com/users/benediktahrens/gists{/gist_id}","starred_url":"https://api.github.com/users/benediktahrens/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/benediktahrens/subscriptions","organizations_url":"https://api.github.com/users/benediktahrens/orgs","repos_url":"https://api.github.com/users/benediktahrens/repos","events_url":"https://api.github.com/users/benediktahrens/events{/privacy}","received_events_url":"https://api.github.com/users/benediktahrens/received_events","type":"User","site_admin":false},"created_at":"2015-08-25T09:07:14Z","updated_at":"2015-08-25T09:07:14Z","body":"Was resolved by PR #135 , closing."}}