diff options
author | 2018-02-20 15:35:25 +0100 | |
---|---|---|
committer | 2018-03-05 14:21:47 +0100 | |
commit | 88f3b5a441a3aaeb637d0b109544fbe71b7560dd (patch) | |
tree | ddbe8c3c4e1e2d773078254b0cef162126503709 /engine/nameops.mli | |
parent | 78551857a41a57607ecfb3fd010e0a9755f47cea (diff) |
Allow universe declarations for [with Definition].
Diffstat (limited to 'engine/nameops.mli')
0 files changed, 0 insertions, 0 deletions