<commit_before>## Changes between Coq 8.8 and Coq 8.9

### ML API

Misctypes

  Syntax for universe sorts and kinds has been moved from `Misctypes`
  to `Glob_term`, as these are turned into kernel terms by
  `Pretyping`.

Proof engine

- More functions have been changed to use `EConstr`, notably the
  functions in `Evd`, and in particular `Evd.define`.

  Note that the core function `EConstr.to_constr` now _enforces_ by
  default that the resulting term is ground, that is to say, free of
  Evars. This is usually what you want, as open terms should be of
  type `EConstr.t` to benefit from the invariants the `EConstr` API is
  meant to guarantee.

  In case you'd like to violate this API invariant, you can use the
  `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
  that setting this flag to false is deprecated so it is only meant to
  be used as to help port pre-EConstr code.

- A few type alias have been deprecated, in all cases the message
  should indicate what the canonical form is. An important change is
  the move of `Globnames.global_reference` to `Names.GlobRef.t`.

### Unit testing

  The test suite now allows writing unit tests against OCaml code in the Coq
  code base. Those unit tests create a dependency on the OUnit test framework.
<commit_msg>Document Smart/Array changes in dev/doc/Changes.md.<commit_after>## Changes between Coq 8.8 and Coq 8.9

### ML API

Misctypes

  Syntax for universe sorts and kinds has been moved from `Misctypes`
  to `Glob_term`, as these are turned into kernel terms by
  `Pretyping`.

Proof engine

- More functions have been changed to use `EConstr`, notably the
  functions in `Evd`, and in particular `Evd.define`.

  Note that the core function `EConstr.to_constr` now _enforces_ by
  default that the resulting term is ground, that is to say, free of
  Evars. This is usually what you want, as open terms should be of
  type `EConstr.t` to benefit from the invariants the `EConstr` API is
  meant to guarantee.

  In case you'd like to violate this API invariant, you can use the
  `abort_on_undefined_evars` flag to `EConstr.to_constr`, but note
  that setting this flag to false is deprecated so it is only meant to
  be used as to help port pre-EConstr code.

- A few type alias have been deprecated, in all cases the message
  should indicate what the canonical form is. An important change is
  the move of `Globnames.global_reference` to `Names.GlobRef.t`.

ML Libraries used by Coq

- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
  Array.Smart.map.
- Uniformization of some names, e.g. Array.Smart.fold_left_map instead
  of Array.smartfoldmap.

### Unit testing

  The test suite now allows writing unit tests against OCaml code in the Coq
  code base. Those unit tests create a dependency on the OUnit test framework.

{'fraction_non_alphanumeric': 0.05667018655403027, 'fraction_numerical': 0.0028159098908834917, 'mean_word_length': 3.7845117845117846, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1310373', 'n_tokens_mistral': 856, 'n_tokens_neox': 831, 'n_words': 429}