Metaprogramming, verified meta-theory and implementation of Coq in Coq
We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.19, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version w.r.t. v1.2.1 are:
MetaCoq Erase -typed
to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v
)Eval
variant that reads back Coq values and can be trusted.Extract Inline
).Extract Inductive
). This allows to target different representations in target languages (typically bool in OCaml).exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 }
becomes exist 1
after typed erasure and removal of constructor parameters, which can be further unboxed to just 1
.The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.
The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
implement_box
by @yforster in https://github.com/MetaCoq/metacoq/pull/999
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2.1-8.18...v1.3.1-8.19
We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.17, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version w.r.t. v1.2.1 are:
MetaCoq Erase -typed
to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v
)Eval
variant that reads back Coq values and can be trusted.Extract Inline
).Extract Inductive
). This allows to target different representations in target languages (typically bool in OCaml).exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 }
becomes exist 1
after typed erasure and removal of constructor parameters, which can be further unboxed to just 1
.The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.
The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
implement_box
by @yforster in https://github.com/MetaCoq/metacoq/pull/999
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2.1-8.18...v1.3.1-8.18
We are happy to announce release 1.3.1 of the MetaCoq project for Coq 8.18, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version w.r.t. v1.2.1 are:
MetaCoq Erase -typed
to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v
)Eval
variant that reads back Coq values and can be trusted.Extract Inline
).Extract Inductive
). This allows to target different representations in target languages (typically bool in OCaml).exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 }
becomes exist 1
after typed erasure and removal of constructor parameters, which can be further unboxed to just 1
.The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.
The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
implement_box
by @yforster in https://github.com/MetaCoq/metacoq/pull/999
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2.1-8.18...v1.3.1-8.18
We are happy to announce release 1.3 of the MetaCoq project for Coq 8.17, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version are (w.r.t. v1.2.1):
MetaCoq Erase -typed
to switch it on. It can be configured with the "live" erasure function inside Coq (see erasure_live_test.v
)Eval
variant that reads back Coq values and can be trusted.Extract Inline
).Extract Inductive
). This allows to target different representations in target languages (typically bool in OCaml).exist nat (fun x : nat => x = 1) 1 p : { x : nat | x = 1 }
becomes exist 1
after typed erasure and removal of constructor parameters, which can be further unboxed to just 1
.The preprint "Verified Extraction from Coq to OCaml" presents the development of the compilation pipeline from Coq to Malfunction/OCaml, including the correctness proofs mentioned above.
The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
This version of MetaCoq was developed by Yannick Forster, Jason Gross, Yann Leray, Matthieu Sozeau and Nicolas Tabareau with contributions from Yishuai Li. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2.1-8.17...v1.3-8.17
This is a minor release synchronising the state of coq-8.17
and coq-8.18
to allow publishing an opam package for Coq 8.18. See https://github.com/MetaCoq/metacoq/releases/tag/v1.2-8.17 for detailed release notes.
extends
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/954
Additionally, the following adaptions were necessary to work with Coq 8.18:
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2-8.17...v1.2.1-8.18
This is a minor release synchronising the state of coq-8.17
and coq-8.18
to allow publishing an opam package for Coq 8.18. See https://github.com/MetaCoq/metacoq/releases/tag/v1.2-8.17 for detailed release notes.
extends
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/954
implement_box
by @yforster in https://github.com/MetaCoq/metacoq/pull/999
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.2-8.17...v1.2.1-8.17
We are happy to announce release 1.2 of the MetaCoq project for Coq 8.17, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version are (w.r.t. v1.1.1):
quotation
library with a work-in-progress proof of Löb's theorem by @JasonGross.MetaCoq Erase
yet.The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
monad_option_map
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/774
match
in on_ind_body
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/778
weakening_env_cored
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/801
hd_error_skipn_iff_In
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/803
make -C erasure/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/805
make -C safechecker/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/810
make uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/811
make -C pcuic/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/812
extends
, fresh_global
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/802
tmFix
point combinator (without unsetting Guard Checking
) by @JasonGross in https://github.com/MetaCoq/metacoq/pull/790
normalisation
into a typeclass by @JasonGross in https://github.com/MetaCoq/metacoq/pull/792
trans_one_inductive_entry
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/789
(only parsing)
to <# x #>
notation by @JasonGross in https://github.com/MetaCoq/metacoq/pull/819
tmQuote
and related template monad definitions by @JasonGross in https://github.com/MetaCoq/metacoq/pull/776
All_Forall
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/821
Proof using
annotations by @JasonGross in https://github.com/MetaCoq/metacoq/pull/849
tmLocateModule
and tmLocateModType
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/855
tmExistingInstance
across localities by @JasonGross in https://github.com/MetaCoq/metacoq/pull/857
.github/dependabot.yml
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/867
DeclarationTypingSig
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/873
Monad
instance for identity monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/881
Monad{Basic,}Ast
to work in any monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/880
Set MetaCoq Template Monad Debug
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/879
consistent_extension_on
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/838
option_instance
universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/893
on_some{,_or_none}
universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/896
Require
s among the MetaCoq modules by @JasonGross in https://github.com/MetaCoq/metacoq/pull/899
Utils.MCFSets
for FSets.FMap*
utils by @JasonGross in https://github.com/MetaCoq/metacoq/pull/901
All_Forall
polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/903
MSets
,FMaps
to use MC{MSets,FSets}
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/907
concurrency
and cancel-in-progress: true
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/910
quote_red
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/912
test-suite/_CoqProject.in
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/915
PCUIC.PCUICMonadAst
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/918
tInt
, tFloat
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/921
isArity
return bool
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/924
tmBind
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/926
concurrency
and cancel-in-progress:true
" by @JasonGross in https://github.com/MetaCoq/metacoq/pull/929
Trel_sig
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/931
conv_pb_leqb
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/932
update-_PluginProject.in
target by @JasonGross in https://github.com/MetaCoq/metacoq/pull/934
concurrency
and cancel-in-progress:true
"" by @JasonGross in https://github.com/MetaCoq/metacoq/pull/937
_dep
versions of Forall2
, All2
, etc by @JasonGross in https://github.com/MetaCoq/metacoq/pull/930
tmOptimizedBind
to avoid quadratic blowup by @JasonGross in https://github.com/MetaCoq/metacoq/pull/936
quote_{All,Forall}2_dep
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/938
cumulSpec0_ind_all
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/933
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.1.1-8.16...v1.2-8.17
We are happy to announce release 1.2 of the MetaCoq project for Coq 8.16, available both as source and through opam. See the website for a detailed overview of the project, introductory material and related articles and presentations.
The main changes in this new version are (w.r.t. v1.1.1):
quotation
library with a work-in-progress proof of Löb's theorem by @JasonGross.MetaCoq Erase
yet.The preprint "Correct and Complete Type Checking and Certified Erasure for Coq, in Coq" presents the development of the sound and complete type checker based on bidirectional typing, the meta-theoretical results (subject reduction, standardization, canonicity and consistency) and the verified erasure procedure of this version of MetaCoq.
MetaCoq integrates Template-Coq, a reification and denotation plugin for Coq terms and global declarations, a Template monad for metaprogramming (including the ability to extract these metaprograms to OCaml for efficiency), a formalisation of Coq's calculus PCUIC in Coq, a relatively efficient, sound and complete type checker for PCUIC, a verified type and proof erasure procedure from PCUIC to untyped lambda calculus and a quotation library. MetaCoq provides a low-level interface to develop certified plugins like translations, compilers or tactics in Coq itself.
You can install MetaCoq directly from sources or using opam install coq-metacoq
.
This release will be included in an upcoming Coq Platform.
The current release includes several subpackages, which can be compiled and installed separately if desired:
utils
, and as coq-metacoq-utils
).common
, coq-metacoq-common
)template-coq
/ coq-metacoq-template
)pcuic
/ coq-metacoq-pcuic
)template-pcuic
and as coq-metacoq-template-pcuic
)safechecker
/ coq-metacoq-safechecker
), usable inside Coq.MetaCoq SafeCheck <term>
command (safechecker-plugin
, coq-metacoq-safechecker-plugin
)erasure
/ coq-metacoq-erasure
), usable inside Coq.MetaCoq Erase <term>
command (erasure-plugin
, coq-metacoq-erasure-plugin
)quotation
/ coq-metacoq-quotation
).translation
/ coq-metacoq-translations
).A good place to start are the files demo.v
, safechecker_test.v
, erasure_test.v
in the test-suite
directory.
MetaCoq is developed by Abhishek Anand, Danil Annenkov, Jakob Botsch Nielsen, Simon Boulier, Cyril Cohen, Yannick Forster, Jason Gross, Meven Lennon-Bertrand, Kenji Maillard, Gregory Malecha, Matthieu Sozeau, Nicolas Tabareau, and Théo Winterhalter. You are welcome to contribute by opening issues and PRs. A MetaCoq Zulip stream is also available.
The MetaCoq Team
monad_option_map
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/774
match
in on_ind_body
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/778
weakening_env_cored
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/801
hd_error_skipn_iff_In
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/803
make -C erasure/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/805
make -C safechecker/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/810
make uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/811
make -C pcuic/ uninstall
no longer builds code first by @JasonGross in https://github.com/MetaCoq/metacoq/pull/812
extends
, fresh_global
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/802
tmFix
point combinator (without unsetting Guard Checking
) by @JasonGross in https://github.com/MetaCoq/metacoq/pull/790
normalisation
into a typeclass by @JasonGross in https://github.com/MetaCoq/metacoq/pull/792
trans_one_inductive_entry
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/789
(only parsing)
to <# x #>
notation by @JasonGross in https://github.com/MetaCoq/metacoq/pull/819
tmQuote
and related template monad definitions by @JasonGross in https://github.com/MetaCoq/metacoq/pull/776
All_Forall
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/821
Proof using
annotations by @JasonGross in https://github.com/MetaCoq/metacoq/pull/849
tmLocateModule
and tmLocateModType
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/855
tmExistingInstance
across localities by @JasonGross in https://github.com/MetaCoq/metacoq/pull/857
.github/dependabot.yml
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/867
DeclarationTypingSig
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/873
Monad
instance for identity monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/881
Monad{Basic,}Ast
to work in any monad by @JasonGross in https://github.com/MetaCoq/metacoq/pull/880
Set MetaCoq Template Monad Debug
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/879
consistent_extension_on
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/838
option_instance
universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/893
on_some{,_or_none}
universe polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/896
Require
s among the MetaCoq modules by @JasonGross in https://github.com/MetaCoq/metacoq/pull/899
Utils.MCFSets
for FSets.FMap*
utils by @JasonGross in https://github.com/MetaCoq/metacoq/pull/901
All_Forall
polymorphic by @JasonGross in https://github.com/MetaCoq/metacoq/pull/903
MSets
,FMaps
to use MC{MSets,FSets}
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/907
concurrency
and cancel-in-progress: true
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/910
quote_red
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/912
test-suite/_CoqProject.in
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/915
PCUIC.PCUICMonadAst
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/918
tInt
, tFloat
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/921
isArity
return bool
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/924
tmBind
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/926
concurrency
and cancel-in-progress:true
" by @JasonGross in https://github.com/MetaCoq/metacoq/pull/929
Trel_sig
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/931
conv_pb_leqb
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/932
update-_PluginProject.in
target by @JasonGross in https://github.com/MetaCoq/metacoq/pull/934
concurrency
and cancel-in-progress:true
"" by @JasonGross in https://github.com/MetaCoq/metacoq/pull/937
_dep
versions of Forall2
, All2
, etc by @JasonGross in https://github.com/MetaCoq/metacoq/pull/930
tmOptimizedBind
to avoid quadratic blowup by @JasonGross in https://github.com/MetaCoq/metacoq/pull/936
quote_{All,Forall}2_dep
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/938
cumulSpec0_ind_all
by @JasonGross in https://github.com/MetaCoq/metacoq/pull/933
Full Changelog: https://github.com/MetaCoq/metacoq/compare/v1.1.1-8.16...v1.2-8.16
MetaCoq 1.1.1 is a patch release of MetaCoq 1.1 removing unsafe extraction directives and with support for printing floating point values.
See https://github.com/MetaCoq/metacoq/releases/tag/v1.1-8.16 for the 1.1 release notes.
MetaCoq 1.1.1 is a patch release of MetaCoq 1.1 removing unsafe extraction directives and with support for printing floating point values.
See https://github.com/MetaCoq/metacoq/releases/tag/v1.1-8.15 for the 1.1 release notes.