diff options
| author | Enrico Tassi | 2015-08-24 07:53:57 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-08-24 07:53:57 +0200 |
| commit | 14c940b332512f313b0b80acd6a17f80721b32fc (patch) | |
| tree | 517889e5326d90cbab408f7adb5cfaecf19b455e /mathcomp/basic/Make | |
| parent | e9163a8339e8c820a127a4a383b0c9427b11cc2a (diff) | |
Compare pattern heads (constants) up to "univs"
So that Universe Polymorphic constants are compared "correctly",
i.e. not discriminated by the pattern filtering phase (verbatim
head comparison) but eventually by unification.
Diffstat (limited to 'mathcomp/basic/Make')
0 files changed, 0 insertions, 0 deletions