aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-17 14:11:13 +0530
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-01-17 14:47:20 +0530
commit9d60a8655f37ee922c662d15b3df0d94a8fd32aa (patch)
treecae315894c17232930cbd0894bfb670a0c4fd6cb /library/library.ml
parent9f5586d88880cbb98c92edfe9c33c76564f1a19c (diff)
Univs: Fix alias computation for VMs, computation of normal form of
match predicates for vm_compute and compile polymorphic definitions to constant code. Add univscompute test-suite file testing VM computations in presence of polymorphic universes.
Diffstat (limited to 'library/library.ml')
0 files changed, 0 insertions, 0 deletions