Make Cumulative, NonCumulative and Private attributes. - #11665

Merged

ppedrot merged 5 commits into

rocq-prover:masterfrom

Zimmi48:cumulative-attr

Mar 20, 2020

Commits on Mar 19, 2020

Update fullGrammar and common.edit_mlg following #11839.
Zimmi48
committed
a5c131b
Make Cumulative, NonCumulative and Private attributes.
Zimmi48
committed
9f834bd
Document all the existing attributes.
Zimmi48
committed
2c785aa
Update fullGrammar, common.edit_mlg and orderedGrammar...
Zimmi48
committed
82960d4
Interpret the Export modifier of Set and Unset as an attribute.
Zimmi48
committed
4b37834