- Added support for
Context
sentencesContext
sentences have been added to the Coq AST that allow implicit arguments to be defined inSection
s.
- Support hints
Hint
sentences have been added to the Coq AST that support a wide range of hints.
- Support options and flags
- Option sentences (i.e.,
Set
andUnset
) have been added to the Coq AST that allow to set and unset arbitrary options and flags.
- Option sentences (i.e.,
- Extended notation definitions
- Notation definitions support a list of identifiers instead of a single identifier.
- Notation definitions support a list of syntax modifiers.
- Initial release as
language-coq
- Initial version forked from hs-to-coq