aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-15 12:20:10 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-10-15 12:20:10 +0200
commit5e1713d8fe9032a3f5c783cce288b409b6fdf816 (patch)
tree7d9eacb8932c4cd3a7958100f3376612c4b7f8ae /pretyping/unification.ml
parent707edf9b1e7310bd213678452950aaaa9e4e95f8 (diff)
Fix test-suite file after moving back to using C as the name
of the record binder for Class C's projections.
Diffstat (limited to 'pretyping/unification.ml')
0 files changed, 0 insertions, 0 deletions