diff options
| author | Pierre-Marie Pédrot | 2018-09-23 17:31:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-23 17:33:00 +0200 |
| commit | a3cbf400d291fe0427f28d2847a0002cb17474dc (patch) | |
| tree | 4a105a3bcda5b67731ae722babeedf83a2ba41f6 /plugins/syntax/string_syntax.ml | |
| parent | 92fbd7383c3897b3932b0ad95afa0982d2d8a7e3 (diff) | |
Fix #8513: EConstr.eq_constr doesn't properly take into account universe variables.
We simply normalize the universe variables before comparing them.
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions