coq - The formal proof system

Age	Commit message (Expand)	Author
2020-12-15	Modify ZArith/Zpower.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Modify micromega/ZMicromega.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Modify QArith/Qreduction.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Modify setoid_ring/Field_theory.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Modify QArith/QArith_base.v to compile with -mangle-names	Jasper Hugunin
2020-12-15	Catch up to where I was last time.	Jasper Hugunin
2020-12-10	Merge PR #12100: Fixing use of argument scopes in patterns + a further cleanu...	coqbot-app[bot]
2020-12-10	Merge PR #13590: Move Azure jobs to GitHub Actions.	coqbot-app[bot]
2020-12-10	Move Azure jobs to GitHub Actions.	Théo Zimmermann
2020-12-10	Merge PR #13605: [osx] disable brew cleanup	coqbot-app[bot]
2020-12-09	Merge PR #13564: Allow all characters in tacn, cmd, ... names. Report duplic...	Clément Pit-Claudel
2020-12-09	Allow any character in a tacn, cmd, ... name	Jim Fehrle
2020-12-09	[osx] disable brew cleanup	Enrico Tassi
2020-12-09	Merge PR #13537: More efficient implementation for substitutions.	coqbot-app[bot]
2020-12-09	Please the god of nitpicking by renaming the shift monoid operations.	Pierre-Marie Pédrot
2020-12-09	Document Esubst API and implementation.	Pierre-Marie Pédrot
2020-12-09	Adding overlays.	Pierre-Marie Pédrot
2020-12-09	Compact representation of identity substitutions.	Pierre-Marie Pédrot
2020-12-09	Optimization: take advantage that we don't use arrays anymore in substitutions.	Pierre-Marie Pédrot
2020-12-09	More efficient implementation for substitutions.	Pierre-Marie Pédrot
2020-12-09	Cleanup substitution API.	Pierre-Marie Pédrot
2020-12-09	Using self-documenting argument names in two exceptions of cases.ml.	Hugo Herbelin
2020-12-09	Constrintern.ml: some naming uniformity.	Hugo Herbelin
2020-12-09	Some documentation in constrintern.ml.	Hugo Herbelin
2020-12-09	Fixing some indentations in constrintern.ml.	Hugo Herbelin
2020-12-09	Constrintern: Code factorization in interning of record fields.	Hugo Herbelin
2020-12-09	Constrintern: Grouping together functions about reference locating.	Hugo Herbelin
2020-12-09	Constrintern cleanup: Centralizing calls to find_appl_head.	Hugo Herbelin
2020-12-09	Fixing support for argument scopes and let-ins while interning cases patterns.	Hugo Herbelin
2020-12-09	Adding functions to returning the def/decl status of an inductive arity.	Hugo Herbelin
2020-12-09	Move addition of parameters in asymmetric mode to first phase of pat interning.	Hugo Herbelin
2020-12-09	Removing a useless explicit use of subscopes in interpreting arguments of a n...	Hugo Herbelin
2020-12-09	Constrintern: As in terms, accept @C for C abbreviation in cases patterns.	Hugo Herbelin
2020-12-09	Constrintern: shortcut in cases pattern interning.	Hugo Herbelin
2020-12-09	Merge PR #13591: [rm] update instructions for windows signing	coqbot-app[bot]
2020-12-09	[rm] announcements to discourse	Enrico Tassi
2020-12-08	Merge PR #13597: Congruence: don't replace error messages by "congruence failed"	coqbot-app[bot]
2020-12-08	Update dev/doc/release-process.md	Enrico Tassi
2020-12-08	Merge PR #13572: [dune] [opam] Disable dune subst in opam files until the ups...	coqbot-app[bot]
2020-12-08	Merge PR #13596: Add a test for cbv over inductive types which feature let-bi...	coqbot-app[bot]
2020-12-08	Congruence: don't replace error messages by "congruence failed"	Gaëtan Gilbert
2020-12-08	Reindent Cctac.cc_tactic	Gaëtan Gilbert
2020-12-08	Add a test for cbv over inductive types which feature let-bindings.	Pierre-Marie Pédrot
2020-12-07	[rm] manual is uploaded by CI	Enrico Tassi
2020-12-07	Merge PR #13588: Add `depopts: coq-native` in coq.opam.docker	coqbot-app[bot]
2020-12-07	[rm] update instructions for windows signing	Enrico Tassi
2020-12-07	Merge PR #13556: Fix spelling in warning entry	coqbot-app[bot]
2020-12-07	Add depopts:coq-native in coq.opam.docker	Erik Martin-Dorel
2020-12-06	Merge PR #13585: [RM] Update changes 13501	coqbot-app[bot]
2020-12-06	[doc] update changes after 13501	Enrico Tassi