aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2015-09-23 16:00:49 +0200
committerMatthieu Sozeau2015-10-02 15:54:10 +0200
commitcc69a4697633e14fc00c9bd0858b38120645464b (patch)
tree6a589f6916cf85bbc008ef3db788db8b90056278 /kernel/nativecode.ml
parentff4d0d98ab0e0e81bd1acf9a7bf4b64913834911 (diff)
Univs: module constraints move to universe contexts as they might
declare new universes (e.g. with).
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions