diff options
| author | Matthieu Sozeau | 2015-11-19 17:48:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-11-19 17:52:26 +0100 |
| commit | 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (patch) | |
| tree | bf7c7746400e696d4fb3f2e7c677e955f8a52066 /kernel/type_errors.ml | |
| parent | 6ababf42b3f03926c30cfbd209436ec83a21769e (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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions