diff options
| author | Gaëtan Gilbert | 2019-05-14 13:10:20 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-14 13:10:20 +0200 |
| commit | d0e258175280152e504a296a05ecbd1920bb17c9 (patch) | |
| tree | 9e7c80e5792c3769d28b04841651d522c4f5c3f1 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 9f11eeefc204bdad029b66f30bc6c52377af63ae (diff) | |
Fix #10161: occur check when defining an algebraic universe.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions