CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS.

• API:
  • Fix: clause_of_term now correctly computes the digest of the whole
    clause, including its attributes

CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS.

• REPL:

  • elpi takes zero or one file (not more) when executing
  • elpi -deps prints a dot file with the direct dependencies of given files.
    Example: elpi -deps *.elpi | xdot -

• API:

  • Change: separate API for scoping AST or builtins. Scoping AST can return more
    than one scoped program, in particular it returns all accumulated code
    with file name and digest. Incidentally it also computes the dependencies
    of each file.
  • New: api to get the dependencies of a scoped program or compilation unit
  • New: api to map compilation units and apply a substitution on the CData
    they contain

CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS.

• Compiler:
  • Change: do not store in the unit the whole program signature (base + unit),
    since this grows quadratically and is a problem in Rocq since some programs
    are made of thausands of units.

CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS.

• Typechecker:
  • Change: when expcting prop or list prop use an excted type of 0 arity
  • Fix: improve error message in case of failed overloading resolution

CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS.

• FFI:
  • Change: Variadic predicates can generate extra goals

CHANGES:

Requires Menhir 20211230 and OCaml 4.14 or above on Linux, Windows and
MacOS 14 (Sonoma). MacOS 15 (Sequoia) and later require OCaml 5.4.

• Typechecker:

  • Change: disallow undeclared data constructors and predicates

• Compiler:

  • New allow builtins to be declared in extension units (not just in the
    base)

• Typechecker:

  • Fix error messages when there is an arity mismatch, i.e. suggest some
    arguments may be missing
  • Change symbols without a declared signature raise a fatal error. Only
    undeclared predicates are tolerated, and only when the inferred type is
    unambiguously prop

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Builtin:
  • Fix pattern_match builtin had the arguments in wrong order (w.r.t. the
    documentation). The pattern is now the second argument.

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Compiler:
  • Fix bug involving spilling and sigma

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Language:

  • New attribute :nooc to disable occur check

• Stdlib:

  • New unsound_unif performing unification without occur check
  • New std.fset and std.fmap that work on ground terms and
    disable occur check

• Compiler:

  • Change raise an error in case of type/typeabbrev collision

• Parser:

  • Fix associativity of =!=> (was not the same as ==>)

CHANGES:

Requires Menhir 20211230 and OCaml 4.13 or above.

• Runtime:
  • Fix bug concerning CHR rules firing on non-fully-dereffed terms