<commit_before>=========================================
= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
=========================================

* Ocaml *

Coq is compiled with -safe-string enabled and requires plugins to do
the same. This means that code using `String` in an imperative way
will fail to compile now. They should switch to `Bytes.t`

* ML API *

We renamed the following functions:

  Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
  Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
  Printer.pr_var_list_decl       -> Printer.pr_compacted_decl
  Printer.pr_var_decl            -> Printer.pr_named_decl
  Nameops.lift_subscript         -> Nameops.increment_subscript

We removed the following functions:

  Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context
  Namegen.to_avoid                      ... equivalent substitute is Names.Id.List.mem

We renamed the following modules:

  Context.ListNamed -> Context.Compacted

The following type aliases where removed

  Context.section_context    ... it was just an alias for "Context.Named.t" which is still available

The module Constrarg was merged into Stdarg.

The following types have been moved and modified:

  local_binder -> local_binder_expr
  glob_binder merged with glob_decl

The following constructors have been renamed:

  LocalRawDef -> CLocalDef
  LocalRawAssum -> CLocalAssum
  LocalPattern -> CLocalPattern

In Constrexpr_ops:

  Deprecating abstract_constr_expr in favor of mkCLambdaN, and
  prod_constr_expr in favor of mkCProdN. Note: the first ones were
  interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
  ones were preserving the original sharing of the type.

In Nameops:

  The API has been made more uniform. New combinators added in the
  "Name" space name. Function "out_name" now fails with IsAnonymous
  rather than with Failure "Nameops.out_name".

Location handling and AST attributes:

  Location handling has been reworked. First, Loc.ghost has been
  removed in favor of an option type, all objects carrying an optional
  source code location have been switched to use `Loc.t option`.

  Storage of location information has been also refactored. The main
  datatypes representing Coq AST (constrexpr, glob_expr) have been
  switched to a generic "node with attributes" representation `'a
  CAst.ast`, which is a record of the form:

```ocaml
type 'a ast = private {
  v   : 'a;
  loc : Loc.t option;
  ...
}
```
  consumers of AST nodes are recommended to use accessor-based pattern
  matching `{ v; loc }` to destruct `ast` object. Creation is done
  with `CAst.make ?loc obj`, where the attributes are optional. Some
  convenient combinators are provided in the module. A typical match:
```
| CCase(loc, a1) -> CCase(loc, f a1)
```
  is now done as:
```
| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
```
  or even better, if plan to preserve the attributes you can wrap your
  top-level function in `CAst.map` to have:

```
| CCase(a1) -> CCase(f a1)
```

  This scheme based on records enables easy extensibility of the AST
  node type without breaking compatibility.

  Not all objects carrying a location have been converted to the
  generic node representation, some of them may be converted in the
  future, for some others the abstraction is not just worth it.

  Thus, we still maintain a `'a Loc.located == Loc.t option * a'`,
  tuple type which should be treated as private datatype (ok to match
  against, but forbidden to manually build), and it is mandatory to
  use it for objects that carry a location. This policy has been
  implemented in the whole code base. Matching a located object hasn't
  changed, however, `Loc.tag ?loc obj` must be used to build one.

In GOption:

  Support for non-synchronous options has been removed. Now all
  options are handled as a piece of normal document state, and thus
  passed to workers, etc... As a consequence, the field
  `Goptions.optsync` has been removed.

In Coqlib / reference location:

  We have removed from Coqlib functions returning `constr` from
  names. Now it is only possible to obtain references, that must be
  processed wrt the particular needs of the client.
  We have changed in constrintern the functions returnin `constr` as
  well to return global references instead.

  Users of `coq_constant/gen_constant` can do
  `Universes.constr_of_global (find_reference dir r)` _however_ note
  the warnings in the `Universes.constr_of_global` in the
  documentation. It is very likely that you were previously suffering
  from problems with polymorphic universes due to using
  `Coqlib.coq_constant` that used to do this. You must rather use
  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
  when constructing terms in ML (see univpoly.txt for more information).

** Tactic API **

- pf_constr_of_global now returns a tactic instead of taking a continuation.
  Thus it only generates one instance of the global reference, and it is the
  caller's responsibility to perform a focus on the goal.

- pf_global, construct_reference, global_reference,
  global_reference_in_absolute_module now return a global_reference
  instead of a constr.

- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
  was very specific. Use tclPROGRESS instead.

** Ltac API **

Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
important things:<commit_msg>Documenting the change of default flag value of Refine.refine.<commit_after>=========================================
= CHANGES BETWEEN COQ V8.6 AND COQ V8.7 =
=========================================

* Ocaml *

Coq is compiled with -safe-string enabled and requires plugins to do
the same. This means that code using `String` in an imperative way
will fail to compile now. They should switch to `Bytes.t`

* ML API *

We renamed the following functions:

  Context.Rel.Declaration.fold   -> Context.Rel.Declaration.fold_constr
  Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr
  Printer.pr_var_list_decl       -> Printer.pr_compacted_decl
  Printer.pr_var_decl            -> Printer.pr_named_decl
  Nameops.lift_subscript         -> Nameops.increment_subscript

We removed the following functions:

  Termops.compact_named_context_reverse ... practical substitute is Termops.compact_named_context
  Namegen.to_avoid                      ... equivalent substitute is Names.Id.List.mem

We renamed the following modules:

  Context.ListNamed -> Context.Compacted

The following type aliases where removed

  Context.section_context    ... it was just an alias for "Context.Named.t" which is still available

The module Constrarg was merged into Stdarg.

The following types have been moved and modified:

  local_binder -> local_binder_expr
  glob_binder merged with glob_decl

The following constructors have been renamed:

  LocalRawDef -> CLocalDef
  LocalRawAssum -> CLocalAssum
  LocalPattern -> CLocalPattern

In Constrexpr_ops:

  Deprecating abstract_constr_expr in favor of mkCLambdaN, and
  prod_constr_expr in favor of mkCProdN. Note: the first ones were
  interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second
  ones were preserving the original sharing of the type.

In Nameops:

  The API has been made more uniform. New combinators added in the
  "Name" space name. Function "out_name" now fails with IsAnonymous
  rather than with Failure "Nameops.out_name".

Location handling and AST attributes:

  Location handling has been reworked. First, Loc.ghost has been
  removed in favor of an option type, all objects carrying an optional
  source code location have been switched to use `Loc.t option`.

  Storage of location information has been also refactored. The main
  datatypes representing Coq AST (constrexpr, glob_expr) have been
  switched to a generic "node with attributes" representation `'a
  CAst.ast`, which is a record of the form:

```ocaml
type 'a ast = private {
  v   : 'a;
  loc : Loc.t option;
  ...
}
```
  consumers of AST nodes are recommended to use accessor-based pattern
  matching `{ v; loc }` to destruct `ast` object. Creation is done
  with `CAst.make ?loc obj`, where the attributes are optional. Some
  convenient combinators are provided in the module. A typical match:
```
| CCase(loc, a1) -> CCase(loc, f a1)
```
  is now done as:
```
| { v = CCase(a1); loc } -> CAst.make ?loc @@ CCase(f a1)
```
  or even better, if plan to preserve the attributes you can wrap your
  top-level function in `CAst.map` to have:

```
| CCase(a1) -> CCase(f a1)
```

  This scheme based on records enables easy extensibility of the AST
  node type without breaking compatibility.

  Not all objects carrying a location have been converted to the
  generic node representation, some of them may be converted in the
  future, for some others the abstraction is not just worth it.

  Thus, we still maintain a `'a Loc.located == Loc.t option * a'`,
  tuple type which should be treated as private datatype (ok to match
  against, but forbidden to manually build), and it is mandatory to
  use it for objects that carry a location. This policy has been
  implemented in the whole code base. Matching a located object hasn't
  changed, however, `Loc.tag ?loc obj` must be used to build one.

In GOption:

  Support for non-synchronous options has been removed. Now all
  options are handled as a piece of normal document state, and thus
  passed to workers, etc... As a consequence, the field
  `Goptions.optsync` has been removed.

In Coqlib / reference location:

  We have removed from Coqlib functions returning `constr` from
  names. Now it is only possible to obtain references, that must be
  processed wrt the particular needs of the client.
  We have changed in constrintern the functions returnin `constr` as
  well to return global references instead.

  Users of `coq_constant/gen_constant` can do
  `Universes.constr_of_global (find_reference dir r)` _however_ note
  the warnings in the `Universes.constr_of_global` in the
  documentation. It is very likely that you were previously suffering
  from problems with polymorphic universes due to using
  `Coqlib.coq_constant` that used to do this. You must rather use
  `pf_constr_of_global` in tactics and `Evarutil.new_global` variants
  when constructing terms in ML (see univpoly.txt for more information).

** Tactic API **

- pf_constr_of_global now returns a tactic instead of taking a continuation.
  Thus it only generates one instance of the global reference, and it is the
  caller's responsibility to perform a focus on the goal.

- pf_global, construct_reference, global_reference,
  global_reference_in_absolute_module now return a global_reference
  instead of a constr.

- The tclWEAK_PROGRESS and tclNOTSAMEGOAL tacticals were removed. Their usecase
  was very specific. Use tclPROGRESS instead.

- The Refine.refine function and its variants now have the unsafe flag turned
  down by default.

** Ltac API **

Many Ltac specific API has been moved in its own ltac/ folder. Amongst other
important things:
{'fraction_non_alphanumeric': 0.07489460938200736, 'fraction_numerical': 0.001793882859449278, 'mean_word_length': 3.9445676274944566, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 29, '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': '4183630', 'n_tokens_mistral': 3226, 'n_tokens_neox': 3114, 'n_words': 1424}