aboutsummaryrefslogtreecommitdiffhomepage
path: root/INSTALL
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-25 21:46:26 +0200
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2014-08-25 21:55:34 +0200
commit109c90efd0dd2bfbeb6c29b263ccd9b2e84e5b9e (patch)
treef7860f13dc18938953ead65c63923aba117d890b /INSTALL
parent12c803053572194c85e4c7b7f347175c7c335858 (diff)
Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible
to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
Diffstat (limited to 'INSTALL')
0 files changed, 0 insertions, 0 deletions