aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorMatthieu Sozeau2014-07-01 22:50:37 +0200
committerMatthieu Sozeau2014-07-01 22:52:08 +0200
commit4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch)
tree8e6367b1936d842b3e56283abc25de2342452884 /kernel/nativecode.mli
parent3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff)
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions