diff options
| author | Hugo Herbelin | 2019-11-13 16:11:11 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 21:02:02 +0100 |
| commit | 4e367eabea7387b5f90c947d75c626336d52d91c (patch) | |
| tree | e882f42f7c2442621cc12d49dcd391ff88110804 /engine/nameops.ml | |
| parent | 5baa841738e60eee65ffc9e313e7cae6f03032e1 (diff) | |
G_constr: Renaming instance -> univ_instance (more specific name).
Diffstat (limited to 'engine/nameops.ml')
0 files changed, 0 insertions, 0 deletions