diff options
| author | Emilio Jesus Gallego Arias | 2020-03-14 05:44:46 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-30 19:05:37 -0400 |
| commit | dc03a4d9a7b527df0c2e571de55fd200666bdb11 (patch) | |
| tree | 7728d1f3a5d3bdf62ddee90ae60aa78e958c8d1e /doc/plugin_tutorial/tuto1/src/simple_declare.ml | |
| parent | ef8f09ef2fe338bb783591abb3cf8e6d5f4d404f (diff) | |
[declareObl] Remove hack w.r.t. to universe normalization.
This was introduced in #6203 , but as far as I can see this
re-normalization step is not necessary.
Diffstat (limited to 'doc/plugin_tutorial/tuto1/src/simple_declare.ml')
0 files changed, 0 insertions, 0 deletions