diff options
| author | Hugo Herbelin | 2018-12-27 12:44:36 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-02-19 15:06:00 +0100 |
| commit | a8a26c87d52c30e5e5d1ba76f1920e8bc68bcd45 (patch) | |
| tree | af00b4d6fa94aa1535829d3772567916024c9a4d /lib | |
| parent | 21bcc5f6fc8db1ccad16dea89f1705a799c1d090 (diff) | |
Notations: Fixing a printing bug with patterns.
Parameters had to be removed in cases_pattern_of_glob_constr.
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions