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-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
Merge PR #13492: Removing non relevant argument binding_kind of GLocalDef.
coqbot-app[bot]
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
Merge PR #13582: Generalize exp_ineq1 and add exp_ineq1_le, which holds foral...
coqbot-app[bot]
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
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
[ci] function to declare projects
Enrico Tassi
2020-12-09
Redefines exp_ineq1 to hold for all non-zero numbers.
Avi Shinnar
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]
[next]