aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-03-25 18:29:28 +0100
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:58:58 +0200
commit62fb849cf9410ddc2d9f355570f4fb859f3044c3 (patch)
tree2f350ca302a46e18840638d20e7ff89beaf2b1f0 /interp/constrintern.mli
parentca318cd0d21ce157a3042b600ded99df6face25e (diff)
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Diffstat (limited to 'interp/constrintern.mli')
0 files changed, 0 insertions, 0 deletions