diff options
| author | Pierre-Marie Pédrot | 2020-07-16 19:34:18 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-12 14:07:13 +0200 |
| commit | a666788182bce7059e6ba41b917b5ca6ab52ae13 (patch) | |
| tree | 00221510912864d8c6bb73c061b1a8478796f5bc /doc/plugin_tutorial/tuto2/src | |
| parent | de16cf5411c2696044d5b17cccb3659d21a79921 (diff) | |
Code simplification around hint manipulation in Class_tactics.
We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/src')
0 files changed, 0 insertions, 0 deletions