0.33

Compatibility with OCaml 5 and Coq 8.17

0.32

• 2020-10 @mpwassell: Add experimental JSON pretty printing
• 2022-03 @fpottier: Support most recent version of PPrint
• 2022-03 @pi8027: Support recent Coq versions tested up to 8.15

0.31

• Peter Sewell (+ Thibaut Pérami): Improve experimental pretty-printing back-end
• Peter Sewell: Some fixes in Tex generation
• Peter Sewell: Add ocamllex-from-string hom to tweak the lexing of a metavar
• Peter Sewell + Thibaut Pérami: Add menhir-start-type hom to specify the top level type of a menhir parser

0.30

2019-10 @palmskog fix Coq library deprecations with Coq 8.10
2019-11 @palmskog HOL library compatibility with kananaskis-13 and master
2019-11 @palmskog explicit Coq universes for metavars, support coq-universe hom for metavars
2019-11 @palmskog fix library and deprecation issues in Coq code from locally-nameless backend
2019-11 @palmskog set -coq_expand_list_types option to false by default

version 0.29

2018-04 @palmskog Coq 8.8 compatibility
2018-05 @alastairreid add -generate_aux_rules false when generating PDF
2019-08 @dstolfa support for comments in Isabelle 2018
2019-08 @JoeyEremondi fix list bounds when subrules are present
2019-08 @JoeyEremondi make error messages consistently formatted with locations
2019-08 @buggymcbugfix explin OTT comment syntax in documentation
2019-08 @rafoo replace `` by $() and add LaTeX packages required by pandoc
2019-08 @Vertmo improvement on generation of lexer and parser (metavars at end, sort tokens, precise OCaml type, update location nl)
2019-08 @rmn30 install menhir_library_extra.mly
2019-08 @hannesm update opam file to 2.0

0.28

• Bugfix: add missing case of Lem auxparam type name hack when it's hom (Brian Campbell)
• copy ocaml_light example sources from svn (rsem/ott/old_pre_github/examples/caml) and partially de-bitrot (Peter Sewell and palmskog for Coq)
• add pointer to VSCode plugin (JoeyEremondi)
• clean opam install of Emacs ott-mode (hannesm, Blaisorblade)

0.27

• add highly experimental -aux_style_rules false option, adding aux info as extra constructor arguments rather than additional rules
• use PPrint instead of OCaml string concatenation in raw and cooked generated pp
• use ocamlc/ocamlopt (not .opt) by @hannesm
• add tex file for macros used in -alltt <filename> output
• fixes for Isabelle and for regression testing (in progress)

version 0.26

• 2017-02-10 Add command-line option -tex_suppress_category <string> to suppress productions or rules with the specified category string.
• 2017-02-13 Add command-line option -tex_suppress_ntr <string> to suppress the grammar rule with that principal nonterminal root.
• 2017-05-28 fixes for Coq 8.5 and 8.6, contributed by @palmskog
• 2017-05-29 - 2017-06-14 Add experimental support for generating a standalone lexer, menhir parser, and pretty printer, as illustrated in tests/menhir_tests/test10menhir
• 2017-07-17 fixes for OCaml -safe-string, contributed by @jpdeplaix
• 2017-09-07 example of "literate" ott spec, in tests/test10literate
• 2017-09-21 use Type instead of Set in Coq list functions, contributed by @palmskog

0.25: Merge pull request #1 from hannesm/fixes

Fixes