diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 12:55:02 +0200 |
| commit | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (patch) | |
| tree | b2884dfed06b740e2b4fd44ff7cec61ca716f906 /pretyping/patternops.ml | |
| parent | c2b76962b407cac8de4465be1e77cf45ff5822d9 (diff) | |
| parent | ae1acfefe52937ea7e3a098137df032363051361 (diff) | |
Merge PR #11977: Generate default names for bound universes of polymorphic definitions
Reviewed-by: ejgallego
Reviewed-by: herbelin
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions