update core-spec for GRefl and re-factored Refl
authorningning <xnningxie@gmail.com>
Thu, 26 Jul 2018 21:20:42 +0000 (17:20 -0400)
committerBen Gamari <ben@smart-cactus.org>
Fri, 27 Jul 2018 16:29:40 +0000 (12:29 -0400)
commite5f3de2cf2f52e7079cbee624ae91beecf663f87
tree8f02e56aecbdad396c73c4a2bd468f4b0ad68d8c
parent3581212e3a5ba42114f47ed83a96322e0e8028ab
update core-spec for GRefl and re-factored Refl

Ticket #15192 introduced the generalized reflexive coercion `GRefl` and
nominal reflexive `Refl`, and removed `CoherenceCo`. Update core-spec
accordingly.  Not sure about notations though; suggestions on more
concise notations would be great.

Test Plan: Read core-spec.pdf

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, thomie, carter

Differential Revision: https://phabricator.haskell.org/D4984
docs/core-spec/CoreLint.ott
docs/core-spec/CoreSyn.ott
docs/core-spec/OpSem.ott
docs/core-spec/core-spec.mng
docs/core-spec/core-spec.pdf