diff options
| author | Pierre-Marie Pédrot | 2019-06-25 13:49:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-06-25 13:49:18 +0200 |
| commit | 56488b97395ddf9c9b1b3737a15fcaabf3f8d50a (patch) | |
| tree | 8a0c50afe918418e4a6d15968f017a9c7130c343 /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | 0c29a6dc3962cf3e6073d9e72a07bf5c279ba0f0 (diff) | |
| parent | d0e258175280152e504a296a05ecbd1920bb17c9 (diff) | |
Merge PR #10162: Fix #10161: occur check when defining an algebraic universe.
Ack-by: SkySkimmer
Ack-by: mattam82
Reviewed-by: ppedrot
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions