Adapt to https://github.com/agda/agda/pull/5289

[jespercockx]

This PR makes the necessary changes to add the three new constructors of the Sort datatype in the reflected syntax which are added to Agda itself in agda/agda#5289.

[jespercockx]

Travis is failing, but I don't see why:

$ agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --html safe.agda

Checking safe (/home/travis/build/agda/agda-stdlib/safe.agda).

/home/travis/build/agda/agda-stdlib/safe.agda:544,1-19

Importing module Debug.Trace using the --rewriting flag from a

module which does not.

when scope checking the declaration

  import Debug.Trace

The command "agda $AGDA_OPTIONS $RTS_OPTIONS -i . -i src/ --html safe.agda" exited with 42.

This seems to be related to the relatively recent change that made --rewriting infective, but I do not see how the changes in this PR have any influence on that.

[gallais]

This seems to be related to the relatively recent change that made --rewriting infective, but I do not see how the changes in this PR have any influence on that.

Could be we were using a commit prior to that change. When you bumped the commit
to the one corresponding to your PR you also included all of the changes that
happened in between.

[jespercockx]

Great, thanks for fixing it! Anything else that still needs to happen before this can be merged? If not I'd like to merge it soon so the main PR for Agda itself can also be merged.

[gallais]

I think it's good to go.