diff options
| author | Pierre-Marie Pédrot | 2019-07-31 12:04:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-31 14:35:23 +0200 |
| commit | 162eefb562aca2c3741ec24d201deb881663e05a (patch) | |
| tree | a2da7727bcc10708ce35908cbf75508899bdd862 /interp/notation_ops.ml | |
| parent | 94dfb7a578e81641a8b816c9a073b81a1c2e4e88 (diff) | |
Remove the universe part from the section variable mechanism.
It was factorized away with the universe declaration entry. Actually,
pomlymorphic universes were declared twice in Declare, once as a context
extension, once as part of the variable itself.
Diffstat (limited to 'interp/notation_ops.ml')
0 files changed, 0 insertions, 0 deletions