Code

A search and replace script#1831

Code

Merged

jdchristensen merged 10 commits intoHoTT:masterHoTT/Coq-HoTT:masterfrom jdchristensen:search-replacejdchristensen/HoTT:search-replaceCopy head branch name to clipboardJan 29, 2024

Commits

Commits on Jan 27, 2024

• Use snrefine instead of simple notypeclasses refine

  jdchristensen

  committed
  b6f28ad

  Copy full SHA for b6f28ad

Commits on Jan 28, 2024

• Add "n" (notypeclasses) to some (s)rapply and (s)refine tactics

  jdchristensen

  committed
  3975076

  Copy full SHA for 3975076

• Remove `{Univalence} when it isn't needed

  jdchristensen

  committed
  38ed29c

  Copy full SHA for 38ed29c

• Change {Univalence} to {Funext} when possible

  jdchristensen

  committed
  b5fcdb8

  Copy full SHA for b5fcdb8

• Remove `{Funext} when not needed

  jdchristensen

  committed
  9825e71

  Copy full SHA for 9825e71

• ReflectiveSubuniverse: remove Univalence and Funext from a Context line

  jdchristensen

  committed
  7aad88d

  Copy full SHA for 7aad88d

• Add .Core to many Require Import lines

  jdchristensen

  committed
  6d32032

  Copy full SHA for 6d32032

• WhiteheadsPrinciple: import Groups.Group instead of Groups

  jdchristensen

  committed
  c30a8ac

  Copy full SHA for c30a8ac

• etc/coqcreplace.py: a script for trying search & replace on files

  jdchristensen

  committed
  a92ccd2

  Copy full SHA for a92ccd2

• etc/coqcstriprequires.py: minor updates

  jdchristensen

  committed
  22f5981

  Copy full SHA for 22f5981