8.11.0+0.11.0: Version 0.11.0:

CHANGES:

• [general] (!) support Coq 8.11, a few datatypes have changed, in
  particular CoqAst handles locations as an AST node, and
  the kernel type includes primitive floats (@ejgallego).
• [general] (!) Now the sertop and serapi OCaml libraries are
  built packed, we've also bumped their compat version number
  (#192 @ejgallego)

8.10.0+0.7.0: CHANGES:

CHANGES:

• [general] (!) support Coq 8.10,
• [serapi] (!) Goals query return type has been modified due to
  upstream changes. (@ejgallego)
• [serlib] Complete (hopefully) serialization for ssreflect ASTs.
  (#73 @ejgallego)
• [general] Drop support for OCaml < 4.07 (#140 @ejgallego)
• [serlib ] JSON serialization for kernel and AST terms (@ejgallego)
• [serapi ] Add Complete support (@ejgallego
  c.f. coq/coq#8766)
• [serlib ] Serlib is now built as a wrapped module (@ejgallego)
• [serapi ] (!) Goals info has been extended to print name metadata if available,
  cc #151 (@ejgallego , suggested by @cpitclaudel)
• [serlib ] JSON support for vernac_expr (@ejgallego)
• [sertop ] (!) Do as Coq upstream and load Coq's stdlib with -R (closes #56)
• [sertop ] Follow Coq upstream and unset indices_matter (closes #157,
  thanks to @palmskog for the report)
• [serapi ] (!) Improve CoqExn answer to have pretty-printed message (improves #162,
  thanks to @cpitclaudel for the request)
• [serlib ] (!) Fix capitalization conventions for a few types in Names
  (closes #167 thanks to @corwin-of-amber for the report)
• [serapi ] (!) Add bullet suggest information to goal query (@corwin-of-amber)
• [sertop ] Add --no_prelude option (closes #176, @ejgallego, request of @darbyhaller)
• [serlib ] (!) Add index to MBId serialization (fixes #150, @ejgallego)
• [serapi ] (!) Add sid parameter to Print (helps #150, @ejgallego, reported by @cpitclaudel)
• [sertop ] Add sertok program for batch serialization of tokens and their source locations (@palmskog)
• [serapi ] (!) Add string-formatted messages to CoqExn and Message
  (@ejgallego closes #184 , closes #162)

8.9.0+0.6.1: Version 0.6.1:

CHANGES:

• [serapi ] Add Parse command to parse a sentence; c.f.
  #117
  (@ejgallego) (cc: @yangky11)
• [sercomp] Add "print" --mode to print the input Coq document
  (@ejgallego) (cc: @Ptival)
• [serlib ] Serialize Universe.t (@ejgallego, request by @yangky11)
• [sercomp] Merge sercomp and compser, add --input parameter to sercomp
  (@palmskog) (cc: @ejgallego)
• [serlib ] Much improved support for serialization of Environ.env
  (@yangky11 and @ejgallego c.f. #118)
• [serapi ] Make sure every command ends with Completed, even if it produced
  an exception (@brando90 and @ejgallego c.f. #124)
• [sercomp] Add --mode=kexp to output the final kernel environment.
  (@ejgallego c.f. #119)
• [serlib ] Serialize more internal environment fields (@ejgallego c.f. #119)
• [serlib ] Improvements in serialization org (@ejgallego)
• [serlib ] Serialize kernel entries (@ejgallego @palmskog)
• [serlib ] Fix critical bug on Constr deserialization; reported by @palmskog,
  fix by @SkySkimmer.
• [sertop] Fix backtrace printing when using --debug (@ejgallego)
• [serlib ] Don't serialize VM values (@ejgallego, bug report by @palmskog)
• [serapi ] Output location on tokenization (@ejgallego , idea by @palmskog)
• [serapi ] Add basic documentation of the protocol (@ejgallego cc #109)

8.9.0+0.6.0: Release 0.6.0 for Coq 8.9.0

CHANGES:

• [general] support Coq 8.9,
• [general] SerAPI now uses Dune as a build system,
• [opam] install sertop.el,
• [serlib] support to serialize kernel environments,
• [serapi] new query Env that tries to print the current kernel environment,
• [serlib] correct field names for CAst,
• [serlib] more robust support for opaque / non-serializable types (#61, #68).
  Thanks to @palmskog,
• [serlib] new option --exn_on_opaque to raise an exception on
  non-serializable types; closes #68, thanks to @palmskog,
• [serlib] serialization test-suite from
  https://github.com/proofengineering/serapi-tests, thanks to
  @palmskog,
• [sercomp] add --mode option to better control output,
• [sercomp] add compser for deserialization (inverse of sercomp)
  (@palmskog),
• [serapi] Allow custom document creation using the NewDoc call.
  Use the --no_init option to avoid automatic creation
  on init. (@ejgallego)
• [sercomp] Allow compilers to output .vo (@ejgallego , suggested by
  @palmskog)
• [sercomp] Serialize top-level vernaculars with their syntactic
  attributes (such as location) (@ejgallego)
• [serapi] Add Assumptions query, at the suggestion of @Armael
  (@ejgallego)
• [sercomp] Disable error resilience mode in compilers; semantics are
  a bit dubious see coq/coq#9204 also #94.
  (@ejgallego, report by @palmskog)
• [sercomp] Add check mode to compilers to check all proofs without
  outputting .vo. (@palmskog)
• [sercomp] Add "hacky" --quick option to skip checking of opaque
  proofs. (@ejgallego, request by @palmskog)
• [sercomp] Add --async_workers option to set maximum number
  of parallel async workers. (@palmskog)
• [sertop] Stop linking Coq plugins statically and load serlib
  plugins when Coq plugins are loaded instead (@ejgallego,
  review by @palmskog)