diff options
| author | Pierre-Marie Pédrot | 2019-05-30 14:17:53 +0200 |
|---|---|---|
| committer | Jim Fehrle | 2019-06-03 03:43:22 -0700 |
| commit | 77fa4df223dc483ebf51fd34d82bb9d3d3405be4 (patch) | |
| tree | c0d1bf310c529bf74bcfbdd5cc1cd11f7b9b276c /doc/plugin_tutorial/tuto1/src | |
| parent | 04398c5fa519b742ff5b97b61bbfa0c9f9d1549c (diff) | |
| parent | 19da31e8e92bb9990e90af162ce1652c6ac71977 (diff) | |
Merge PR #10269: Checker: don't use monomorphic universes attached to a constant
Reviewed-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src')
0 files changed, 0 insertions, 0 deletions