aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/recordops.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-04-02 17:24:30 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:58:58 +0200
commitb17c1e128fad2e84ebe4e4742b47bd67d88c56d6 (patch)
treebac92e1b2ffee60a4a33618c29d2a61b49bdb64a /pretyping/recordops.mli
parenta2fce6d14d00a437466a1f7e3b53a77229f87980 (diff)
Fix restrict_universe_context to not remove useful constraints.
Diffstat (limited to 'pretyping/recordops.mli')
0 files changed, 0 insertions, 0 deletions