diff options
| author | Pierre-Marie Pédrot | 2019-03-18 10:31:24 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-03-18 10:31:24 +0100 |
| commit | 68dd7ff4aa71ac35a5023a2f3d471af08c0d276e (patch) | |
| tree | 6f97b7f26d6676d6c1db8b71a62eb88a9ca1bdaa /pretyping/pattern.ml | |
| parent | 0fc0b5f74a402c1393b485543eca6fbd63bafc61 (diff) | |
| parent | 05843c92e0fe96f09c7c4cb3d55376b99e6ea16b (diff) | |
Merge PR #9794: Use local universe names when printing universe inconsistency
Reviewed-by: ppedrot
Diffstat (limited to 'pretyping/pattern.ml')
0 files changed, 0 insertions, 0 deletions