aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.mllib
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 22:26:18 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-09-17 22:26:18 +0200
commitd9736dae4168927f735ca4f60b61a83929ae4435 (patch)
tree4afd85aee98945c458f210261ccc4265298e4475 /pretyping/pretyping.mllib
parentf96dc97f48df5d0fdf252be5f28478a58be77961 (diff)
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Diffstat (limited to 'pretyping/pretyping.mllib')
0 files changed, 0 insertions, 0 deletions