Closed L-TChen closed 2 years ago
This PR is to make cubical compatible with the recent PR https://github.com/agda/agda/pull/5716, since extendContext takes an extra variable of type String in the reflection API.
cubical
extendContext
String
Note that this PR should not be merged unless https://github.com/agda/agda/pull/5716 is merged.
The PR agda/agda#5716 is merged! Please merge this PR to update if you'd like to.
This PR is to make
cubical
compatible with the recent PR https://github.com/agda/agda/pull/5716, sinceextendContext
takes an extra variable of typeString
in the reflection API.Note that this PR should not be merged unless https://github.com/agda/agda/pull/5716 is merged.