diff options
| author | Pierre-Marie Pédrot | 2019-05-30 14:17:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-30 14:17:53 +0200 |
| commit | 7032085c809993d6a173e51aec447c02828ae070 (patch) | |
| tree | c0d1bf310c529bf74bcfbdd5cc1cd11f7b9b276c /doc/plugin_tutorial/tuto1/src/simple_check.ml | |
| 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/simple_check.ml')
0 files changed, 0 insertions, 0 deletions