aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-06-30 12:55:02 +0200
committerEmilio Jesus Gallego Arias2020-06-30 12:55:02 +0200
commitbffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (patch)
treeb2884dfed06b740e2b4fd44ff7cec61ca716f906 /proofs
parentc2b76962b407cac8de4465be1e77cf45ff5822d9 (diff)
parentae1acfefe52937ea7e3a098137df032363051361 (diff)
Merge PR #11977: Generate default names for bound universes of polymorphic definitions
Reviewed-by: ejgallego Reviewed-by: herbelin
Diffstat (limited to 'proofs')
0 files changed, 0 insertions, 0 deletions