Code

Removing hints from the repo#3680

Code

Merged

gebner merged 4 commits intomasterFStarLang/FStar:masterfrom _nik_no_hintsFStarLang/FStar:_nik_no_hintsCopy head branch name to clipboardJan 15, 2025

+67-545,989

Commits

Commits on Jan 15, 2025

• delete all hint files

  nikswamy

  committed
  64cd791

  Copy full SHA for 64cd791

• fix a few files that were relying on disabling context_pruning

  nikswamy

  committed
  be9d298

  Copy full SHA for be9d298

• remove hints from makefiles and project files

  nikswamy

  committed
  d35a5e4

  Copy full SHA for d35a5e4

• Remove hints CI.

  gebner

  committed
  b09c4e8

  Copy full SHA for b09c4e8