diff options
| author | Emilio Jesus Gallego Arias | 2020-02-02 13:36:41 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-02 13:36:41 +0100 |
| commit | 9c461520c56232e7f7fbebd5134f9e902be1b597 (patch) | |
| tree | 951010c77baf8e61944fa07db47521737594b6ed /engine/eConstr.ml | |
| parent | 4a4e300a8db1907ec94686e22a84078b39fc6f8a (diff) | |
| parent | 0fde47c049322736bbe8ac46d616c2fa3c59c6dd (diff) | |
Merge PR #11326: Refactoring part of #11120 about printing applied global references
Reviewed-by: ejgallego
Diffstat (limited to 'engine/eConstr.ml')
0 files changed, 0 insertions, 0 deletions