index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2020-12-14
Merge PR #13523: [envars] honor file "coq_environment.txt"
Pierre-Marie Pédrot
2020-12-14
Merge PR #13626: [ci] update doc for overlays
coqbot-app[bot]
2020-12-14
Update dev/tools/pin-ci.sh
Enrico Tassi
2020-12-14
[ci] simplify script to pin ci projects
Enrico Tassi
2020-12-14
[ci] fix code to check if the overlay is valid
Enrico Tassi
2020-12-14
Do not rely on Reductionops to recognize canonical projections.
Pierre-Marie Pédrot
2020-12-14
Remove most of Reductionops.*_state functions.
Pierre-Marie Pédrot
2020-12-14
Reuse the cache everywhere possible in Clenv.
Pierre-Marie Pédrot
2020-12-14
Store the metasubst cache in clenvs.
Pierre-Marie Pédrot
2020-12-14
Make the clenv type private and provide a creation function.
Pierre-Marie Pédrot
2020-12-14
Cache meta access in meta_instance.
Pierre-Marie Pédrot
2020-12-14
Merge PR #13613: [changes] mark #12765 as experimental
coqbot-app[bot]
2020-12-14
Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction P...
Pierre-Marie Pédrot
2020-12-13
Update dev/ci/user-overlays/README.md
Enrico Tassi
2020-12-13
Merge PR #13619: doc: Clarify the status of simpl vs cbn
coqbot-app[bot]
2020-12-13
Add changelog for #13509.
Hugo Herbelin
2020-12-13
Removing unused internal introduction-patterns flag assert_style.
Hugo Herbelin
2020-12-13
Removing flag "Bracketing Last Introduction Pattern".
Hugo Herbelin
2020-12-12
Merge PR #13620: Use a registered printer for tactic coercion failure.
coqbot-app[bot]
2020-12-12
[ci] update doc for overlays
Enrico Tassi
2020-12-12
Tweak constr_matching so as to make it tail-rec on projection expansion.
Pierre-Marie Pédrot
2020-12-12
Small API encapsulation inside Redexpr.
Pierre-Marie Pédrot
2020-12-12
Extrude the computation of redexp flags in reduce.
Pierre-Marie Pédrot
2020-12-12
Split the intepretation of red_exprs in two phases.
Pierre-Marie Pédrot
2020-12-12
Generalize the type of red_expr w.r.t. the type of flags they contain.
Pierre-Marie Pédrot
2020-12-12
Merge PR #13603: [ci] function to declare projects
coqbot-app[bot]
2020-12-11
Revert removal of eoi_entry in #13447
Jim Fehrle
2020-12-11
Merge PR #13492: Removing non relevant argument binding_kind of GLocalDef.
coqbot-app[bot]
2020-12-11
Fast path in tclPROGRESS.
Pierre-Marie Pédrot
2020-12-11
Use a registered printer for tactic coercion failure.
Pierre-Marie Pédrot
2020-12-11
doc: Clarify the status of simpl vs cbn
Clément Pit-Claudel
2020-12-11
Removing non relevant argument binding_kind of GLocalDef.
Hugo Herbelin
2020-12-11
Merge PR #13519: Better primitive type support in custom string and numeral n...
coqbot-app[bot]
2020-12-11
Merge PR #13611: Clarify changelog categories.
Clément Pit-Claudel
2020-12-11
Merge PR #13612: Bump reference to 8.12 refman following unexpected 8.12.2 re...
Clément Pit-Claudel
2020-12-11
Merge PR #13540: Clean support of primitive integers
Pierre-Marie Pédrot
2020-12-11
Bench: add .log extension to .stdout/stderr files
Gaëtan Gilbert
2020-12-11
Document the manual tasks that I need to do at each release.
Théo Zimmermann
2020-12-11
Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds foral...
coqbot-app[bot]
2020-12-11
[changes] mark #12765 as experimental
Enrico Tassi
2020-12-11
Bump reference to 8.12 refman following unexpected 8.12.2 release.
Théo Zimmermann
2020-12-11
Clarify changelog categories.
Théo Zimmermann
2020-12-10
Merge PR #13608: Changelog for 8.12.2.
coqbot-app[bot]
2020-12-10
Changelog for 8.12.2.
Théo Zimmermann
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
[ci] update url of autosubst
Enrico Tassi
2020-12-10
[ci] remove old overlays so that people don't copy them
Enrico Tassi
2020-12-10
[ci] simplify overlay scripts
Enrico Tassi
2020-12-10
Move Azure jobs to GitHub Actions.
Théo Zimmermann
[prev]
[next]