v1.3.1-8.20

This is a minor update of Equations, now compatible with Coq 8.20. The main changes are fixes in the funelim tactic and simplification engine to avoid trying to simplify unrelated hypotheses (those under "block" markers). which sometimes led to slowing down the tactic.
Also includes performance improvements by @ppedrot.

What's Changed

• Remove a useless evar normalization in Equations.define_by_eqs. by @ppedrot in #579
• Adapt to coq/coq#18327 (projection opacity) by @rlepigre in #574
• Adapt to coq/coq#18603 (print_rel_context takes evar map) by @SkySkimmer in #581
• Adapt to coq/coq#18224 by @proux01 in #578
• Don't pierce Qed in debug message (adapt to coq/coq#18422) by @SkySkimmer in #586
• Adapt to coq/coq#18546. by @rlepigre in #582
• Adapt to coq/coq#18864 (search_guard can handle evars) by @SkySkimmer in #587
• Adapt w.r.t. coq/coq#18911. by @ppedrot in #588
• Adapt w.r.t. coq/coq#18935. by @ppedrot in #590
• Adapt to coq/coq#18938 (EConstr.ERelevance) by @SkySkimmer in #591
• Use correct scheme kind in example by @SkySkimmer in #594
• Adapt to Coq PR #18743: search_guard is now able to decide late if a recursive definition is a fix or a cofix by @herbelin in #584
• Fix simplify breaking the transparency/opaque status of constants a… by @mattam82 in #593
• Centralize the use of Tactics.assert_before_replacing. by @ppedrot in #601
• Revert "Fix simplify breaking the transparency/opaque status of constants a…" by @mattam82 in #603
• Fix funelim and add a funelim_nosimp variant which does not try to … by @mattam82 in #604
• Replace the outdated "Below" hint database with a rec_decision data… by @mattam82 in #602
• Adapt to Coq PR #18795 (more uniform API for declare.ml) by @herbelin in #599
• Adapt w.r.t. coq/coq#19120. by @ppedrot in #605
• Remove a good part of the sources of abusive typing by @ppedrot in #606
• Turn context_map into a record. by @ppedrot in #607
• Enforce more static typing by @ppedrot in #608
• Adapt w.r.t. coq/coq#19313. by @ppedrot in #611
• adapt to coq/coq#19300 by @gares in #610

Full Changelog: v1.3-8.19...v1.3.1-8.20

Equations 1.3 for Coq 8.19

See the release notes for Equations 1.3

Equations 1.3 for Coq 8.18

Equations 1.3

This is a new major release of Equations, working with Coq 8.18. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3 for Coq 8.17

Equations 1.3

This is a new major release of Equations, working with Coq 8.17. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3 for Coq 8.16

Equations 1.3

This is a new major release of Equations, working with Coq 8.16. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3 for Coq 8.15

Equations 1.3

This is a new major release of Equations, working with Coq 8.15. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3 for Coq 8.13

Equations 1.3

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3 for Coq 8.14

Equations 1.3

This is a new major release of Equations, working with Coq 8.14. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3beta2 for Coq 8.13

Equations 1.3

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Enhancements of pattern interpretation

  No explicit shadowing of pattern variables is allowed anymore. This fixes numerous bugs where
  generated implicit names introduced by the elaboration of patterns could shadow user-given names,
  leading to incorrect names in right-hand sides and confusing environments.

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.

• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.

• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.

• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in v1.3beta2:

• Fix #399: allow simplification in indices when splitting a variable, to expose the head of the index.
• Fix #389: error derving EqDec in HoTT variant.
• Allow universe binder annotations @{} on Equations definitions.
• Fix "struct" parsing issue that required a reset of Coq sometimes
• POTENTIAL SOURCE OF INCOMPATIBILITY:
  Pattern enhancements: no explicit shadowing of pattern variables is allowed anymore. Fix numerous bugs where generated implicit names introduced by the elaboration of patterns could shadow user-given names, leading to incorrect names in right-hand sides.

Fixed in 1.3beta1:

• #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
• #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
• #372, #194: funelim applied to a partial application failing
• #354: support for building values in SProp
• #353: name capture problem in presence of modules
• #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
• #325: properly inline all Equations helper constants during Extraction

Equations 1.3beta1 for Coq 8.13

Equations 1.3

This is a new major release of Equations, working with Coq 8.13. This version adds an improved syntax (less ;-separation), integration with the Coq-HoTT library and numerous bug fixes. See the reference manual for details.

This version introduces minor breaking changes along with the following features:

• Improved syntax for "concise" clauses separated by |, at top-level or inside with subprograms.
  We no longer require to separate them by ;. For example, the following definition is now accepted:

  Equations foo : nat -> nat := 
    | 0 => 1
    | S n => S (foo n).

  The old syntax is however still supported for backwards compatibility.
• Multiple patterns can be separated by , in addition to |, as in:

  Equations trans {A} {x y z : A} (e : x = y) (e' : y = z) : x = z := | 1, 1 => 1.

• Require Import Equations.Equations. does not work anymore.
  One has to use Require Import Equations.Prop.Equations to load the plugin's default instance where equality is in Prop. From Equations Require Import Equations is unaffected.
• Use Require Import Equations.HoTT.All to use the HoTT variant of the library compatible with the Coq HoTT library
  The plugin then reuses the definition of paths from the HoTT library and all its constructions are universe polymorphic. As for the HoTT library alone, coq must be passed the arguments -noinit -indices-matter to use the library and plugin. The coq-equations opam package depends optionally on coq-hott, so if coq-hott is installed before it, coq-equations will automatically install the HoTT library variant in addition to the standard one. This variant of Equations allows to write very concise dependent pattern-matchings on equality:

  Require Import Equations.HoTT.All.
  Equations sym {A} {x y : A} (e : x = y) : y = x := | 1 => 1.

• New attribute #[tactic=tac] to set locally the default tactic to solve remaining holes.
  The goals on which the tactic applies are now always of the form Γ |- τ where Γ is the context where the hole was introduced and τ the expected type, even when using the Obligation machinery to solve them, resulting in a possible incompatibility if the obligation tactic treated the context differently than the conclusion. By default, the program_simpl tactic performs a simpl call before introducing the hypotheses, so you might need to add a simpl in * to your tactics.
• New attributes #[derive(equations=yes,no, eliminator=yes|no)] can be used in place of the (noeqns, noind) flags which are deprecated.

Fixed in this version:

∗ #329: improved strengthening avoiding to abstract over recursive definitions which would not pass the guardness checker. This can simplify the produced terms, avoiding unnecessary "commutative cuts".
∗ #321: warn rather than error when using Equations? and no subgoals are left. This will leave a proof state with no subgoals, that must be closed using a Qed or Defined (similarly to Coq’s #[refine] Instance command).
∗ #372, #194: funelim applied to a partial application failing
∗ #354: support for building values in SProp
∗ #353: name capture problem in presence of modules
∗ #335: provide an alias Equations Derive to not conflict with QuickChick’s Derive
∗ #325: properly inline all Equations helper constants during Extraction