Code

Typeclass hints#2254

Code

Open

patrick-nicodemus wants to merge 5 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom patrick-nicodemus:tc_fixespatrick-nicodemus/HoTT:tc_fixesCopy head branch name to clipboard

Commits

Commits on Mar 14, 2025

• first round of patches after commits

  

  Patrick Nicodemus

  authored and

  Patrick Nicodemus

  committed
  76811bc

  Copy full SHA for 76811bc

• some more exports

  

  Patrick Nicodemus

  committed
  8daae09

  Copy full SHA for 8daae09

• Spelling and style changes

  

  Patrick Nicodemus

  authored and

  Patrick Nicodemus

  committed
  35cd5db

  Copy full SHA for 35cd5db

• Fixed reviewer comments.

  

  Patrick Nicodemus

  committed
  9cdc153

  Copy full SHA for 9cdc153

• all exports

  

  Patrick Nicodemus

  committed
  26b3e29

  Copy full SHA for 26b3e29