Mtac2 for 8.10

See CHANGES for details

Mtac2 1.1 for Coq 8.9

This release includes, among several bug-fixes:

• Several performance improvements, mostly related to reducing the number of universes required for Mtac2 programs.
• A new primitive for creating inductive definitions, still in beta.
• A richer type for goals, including the possibility to change a hypothesis's type, and to ensure via typing that a goal has the Metavar constructor (formerly Goal).

Mtac2 1.1 for Coq 8.8

This release includes, among several bug-fixes:

• Several performance improvements, mostly related to reducing the number of universes required for Mtac2 programs.
• A new primitive for creating inductive definitions, still in beta.
• A richer type for goals, including the possibility to change a hypothesis's type, and to ensure via typing that a goal has the Metavar constructor (formerly Goal).

Mtac2 1.0 for Coq 8.8

v1.0.1-coq8.8

Merge branch 'nocumul-8.8' into coq-8.8

Mtac2 1.0 for Coq 8.7

v1.0.0-coq8.7

Fix _CoqProject.