{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/6414","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/6414/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/6414/comments","events_url":"https://api.github.com/repos/coq/coq/issues/6414/events","html_url":"https://github.com/coq/coq/issues/6414","id":281623523,"number":6414,"title":"Document universe \"normalization\"","user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"labels":[{"id":649046438,"url":"https://api.github.com/repos/coq/coq/labels/kind:%20documentation","name":"kind: documentation","color":"990000","default":false},{"id":757883976,"url":"https://api.github.com/repos/coq/coq/labels/priority:%20high","name":"priority: high","color":"F38238","default":false}],"state":"open","locked":false,"assignee":{"login":"mattam82","id":98373,"avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false},"assignees":[{"login":"mattam82","id":98373,"avatar_url":"https://avatars1.githubusercontent.com/u/98373?v=4","gravatar_id":"","url":"https://api.github.com/users/mattam82","html_url":"https://github.com/mattam82","followers_url":"https://api.github.com/users/mattam82/followers","following_url":"https://api.github.com/users/mattam82/following{/other_user}","gists_url":"https://api.github.com/users/mattam82/gists{/gist_id}","starred_url":"https://api.github.com/users/mattam82/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/mattam82/subscriptions","organizations_url":"https://api.github.com/users/mattam82/orgs","repos_url":"https://api.github.com/users/mattam82/repos","events_url":"https://api.github.com/users/mattam82/events{/privacy}","received_events_url":"https://api.github.com/users/mattam82/received_events","type":"User","site_admin":false}],"milestone":{"url":"https://api.github.com/repos/coq/coq/milestones/5","html_url":"https://github.com/coq/coq/milestone/5","labels_url":"https://api.github.com/repos/coq/coq/milestones/5/labels","id":2550427,"number":5,"title":"8.8","description":"","creator":{"login":"maximedenes","id":647105,"avatar_url":"https://avatars1.githubusercontent.com/u/647105?v=4","gravatar_id":"","url":"https://api.github.com/users/maximedenes","html_url":"https://github.com/maximedenes","followers_url":"https://api.github.com/users/maximedenes/followers","following_url":"https://api.github.com/users/maximedenes/following{/other_user}","gists_url":"https://api.github.com/users/maximedenes/gists{/gist_id}","starred_url":"https://api.github.com/users/maximedenes/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/maximedenes/subscriptions","organizations_url":"https://api.github.com/users/maximedenes/orgs","repos_url":"https://api.github.com/users/maximedenes/repos","events_url":"https://api.github.com/users/maximedenes/events{/privacy}","received_events_url":"https://api.github.com/users/maximedenes/received_events","type":"User","site_admin":false},"open_issues":124,"closed_issues":228,"state":"open","created_at":"2017-05-30T13:02:47Z","updated_at":"2017-12-15T21:36:24Z","due_on":null,"closed_at":null},"comments":4,"created_at":"2017-12-13T04:42:17Z","updated_at":"2017-12-16T00:04:25Z","closed_at":null,"author_association":"MEMBER","body":"Please document the several `nf_*` functions spread over `Evarutil`, `Evd`, and `Universes`. In particular, we need:\r\n\r\n- detailed documentation of the purpose and cost of each one\r\n- detailed documentation on how they are supposed to work together. For example, what is the proper order of calls?\r\n- detailed relative documentation, which ones are a superset of others, and which ones are the composition of available substitution operators.\r\n\r\nA few of the functions:\r\n```ocaml\r\nevarutil: val nf_evar :  evar_map -> constr -> constr\r\nevarutil: val j_nf_evar :  evar_map -> unsafe_judgment -> unsafe_judgment\r\nevarutil: val jl_nf_evar : evar_map -> unsafe_judgment list -> unsafe_judgment list\r\nevarutil: val jv_nf_evar : evar_map -> unsafe_judgment array -> unsafe_judgment array\r\nevarutil: val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment\r\nevarutil: val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t\r\nevarutil: val nf_rel_context_evar : evar_map -> rel_context -> rel_context\r\nevarutil: val nf_env_evar : evar_map -> env -> env\r\nevarutil: val nf_evar_info : evar_map -> evar_info -> evar_info\r\nevarutil: val nf_evar_map : evar_map -> evar_map\r\nevarutil: val nf_evar_map_undefined : evar_map -> evar_map\r\nevarutil: val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr\r\nevarutil: val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)\r\nevarutil: val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst\r\nevarutil: val nf_evar_map_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)\r\nevd:      val nf_univ_variables : evar_map -> evar_map * Univ.universe_subst\r\nevd:      val nf_constraints : evar_map -> evar_map\r\nevd:      val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map\r\nevd:      val normalize_universe : evar_map -> Univ.Universe.t -> Univ.Universe.t\r\nevd:      val normalize_universe_instance : evar_map -> Univ.Instance.t -> Univ.Instance.t\r\nuniverses:val nf_evars_and_universes_opt_subst : (existential -> constr option) -> universe_opt_subst -> constr -> constr\r\nuniverses:val normalize_context_set : ContextSet.t -> universe_opt_subst -> LSet.t -> (universe_opt_subst * LSet.t) in_universe_context_set\r\nuniverses:val normalize_univ_variables : universe_opt_subst -> universe_opt_subst * LSet.t * LSet.t * universe_subst\r\nuniverses:val normalize_univ_variable : find:(Level.t -> Universe.t) -> update:(Level.t -> Universe.t -> Universe.t) -> Level.t -> Universe.t\r\nuniverses:val normalize_univ_variable_opt_subst : universe_opt_subst ref -> (Level.t -> Universe.t)\r\nuniverses:val normalize_univ_variable_subst : universe_subst ref -> (Level.t -> Universe.t)\r\nuniverses:val normalize_universe_opt_subst : universe_opt_subst ref -> (Universe.t -> Universe.t)\r\nuniverses:val normalize_universe_subst : universe_subst ref -> (Universe.t -> Universe.t)\r\nevardefine.mli:val env_nf_evar : evar_map -> env -> env\r\nevardefine.mli:val env_nf_betaiotaevar : evar_map -> env -> env\r\nreductionops.mli:val nf_evar : evar_map -> constr -> constr\r\n```"},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/352141772","html_url":"https://github.com/coq/coq/issues/6414#issuecomment-352141772","issue_url":"https://api.github.com/repos/coq/coq/issues/6414","id":352141772,"user":{"login":"ejgallego","id":7192257,"avatar_url":"https://avatars2.githubusercontent.com/u/7192257?v=4","gravatar_id":"","url":"https://api.github.com/users/ejgallego","html_url":"https://github.com/ejgallego","followers_url":"https://api.github.com/users/ejgallego/followers","following_url":"https://api.github.com/users/ejgallego/following{/other_user}","gists_url":"https://api.github.com/users/ejgallego/gists{/gist_id}","starred_url":"https://api.github.com/users/ejgallego/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ejgallego/subscriptions","organizations_url":"https://api.github.com/users/ejgallego/orgs","repos_url":"https://api.github.com/users/ejgallego/repos","events_url":"https://api.github.com/users/ejgallego/events{/privacy}","received_events_url":"https://api.github.com/users/ejgallego/received_events","type":"User","site_admin":false},"created_at":"2017-12-16T00:04:25Z","updated_at":"2017-12-16T00:04:25Z","author_association":"MEMBER","body":"Oh indeed I copied too much, sorry. Comment amended."}}
{"actor":{"display_login":"ejgallego"}}