Code

Allow attributes on record fields#2192

Code

Merged

aseemr merged 22 commits intoFStarLang:masterFStarLang/FStar:masterfrom mateuszbujalski:matbuj_record_field_attributesmateuszbujalski/FStar:matbuj_record_field_attributesCopy head branch name to clipboardFeb 12, 2021

+1,191-376

Commits

Commits on Dec 23, 2020

• allow more than one attributes on the binders

  mateuszbujalski

  committed
  4b7757a

  Copy full SHA for 4b7757a

Commits on Dec 30, 2020

• Enable attributes on non-implicit binders (needs fixing as it introduces new shift/reduce conflicts in the parser)

  mateuszbujalski

  committed
  453849d

  Copy full SHA for 453849d

• Add support for attributes on record fields

  mateuszbujalski

  committed
  e9a170f

  Copy full SHA for e9a170f

• snap

  mateuszbujalski

  committed
  4da1b26

  Copy full SHA for 4da1b26

• fix test

  mateuszbujalski

  committed
  e9d1c67

  Copy full SHA for e9d1c67

• drop outdated comment

  mateuszbujalski

  committed
  1c502d9

  Copy full SHA for 1c502d9

Commits on Jan 11, 2021

• Add a test for attributes on explicit and implicit binders

  mateuszbujalski

  committed
  ea76d8f

  Copy full SHA for ea76d8f

• Merge remote-tracking branch 'upstream/master' into matbuj_record_field_attributes

  mateuszbujalski

  committed
  e001b0c

  Copy full SHA for e001b0c

• regenerate parse.fsi

  mateuszbujalski

  committed
  96a4994

  Copy full SHA for 96a4994

Commits on Feb 10, 2021

• Merge branch 'matbuj_record_field_attributes' of https://github.com/mateuszbujalski/FStar into matbuj_attrs

  nikswamy

  committed
  84f4bfa

  Copy full SHA for 84f4bfa

• addressing conflicts in the grammar

  nikswamy

  committed
  e2b0865

  Copy full SHA for e2b0865

• kick ci

  nikswamy

  committed
  d3884c9

  Copy full SHA for d3884c9

• [@@@ for binder attributes

  nikswamy

  committed
  0f60de4

  Copy full SHA for 0f60de4

• update test cases to use @@@

  nikswamy

  committed
  a806100

  Copy full SHA for a806100

• merging master in

  nikswamy

  committed
  2c0d117

  Copy full SHA for 2c0d117

• snap

  nikswamy

  committed
  f464dbb

  Copy full SHA for f464dbb

• snap

  nikswamy

  committed
  90164cf

  Copy full SHA for 90164cf

• Remove todos as nik has fixed them

  mateuszbujalski

  committed
  2b3cd39

  Copy full SHA for 2b3cd39

Commits on Feb 11, 2021

• Merge remote-tracking branch 'upstream/master' into matbuj_record_field_attributes

  mateuszbujalski

  committed
  a1348cd

  Copy full SHA for a1348cd

Commits on Feb 12, 2021

• Add test for multiple attributes on a binder

  mateuszbujalski

  committed
  97a9429

  Copy full SHA for 97a9429

• Merge remote-tracking branch 'upstream/master' into matbuj_record_field_attributes

  mateuszbujalski

  committed
  23a90d8

  Copy full SHA for 23a90d8

• revert changes to FStar.Tactics.Util

  mateuszbujalski

  committed
  022d294

  Copy full SHA for 022d294