aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/cbv.mli
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-11-19 17:48:32 +0100
committerGravatar Matthieu Sozeau <matthieu.sozeau@inria.fr>2015-11-19 17:52:26 +0100
commit9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (patch)
treebf7c7746400e696d4fb3f2e7c677e955f8a52066 /pretyping/cbv.mli
parent6ababf42b3f03926c30cfbd209436ec83a21769e (diff)
Fix bug #4433, removing hack on evars appearing in a pattern from a
constr, and the associated signature, not needed anymore. Update CHANGES, no evar_map is produced by pattern_of_constr anymore.
Diffstat (limited to 'pretyping/cbv.mli')
0 files changed, 0 insertions, 0 deletions