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-04-21
Merge PR #12116: Fixing #12045: missing normalization in conclusion of custom...
Pierre-Marie Pédrot
2020-04-21
Merge PR #12014: [stdlib] Add properties of operations on vectors
Hugo Herbelin
2020-04-21
Merge PR #11883: Fix #7812: autounfold's behavior depends on file names
Hugo Herbelin
2020-04-20
Merge PR #12038: Improve undeclared goption key messages.
Gaëtan Gilbert
2020-04-20
Merge PR #12126: TIMEFMT: Display the output file name
Gaëtan Gilbert
2020-04-20
Merge PR #12026: Granting coqdoc wish #7093: definitions link to themselves s...
Lysxia
2020-04-20
Adding change log for PR #12026 (definitions in coqdoc link to themselves).
Hugo Herbelin
2020-04-20
Granting coqdoc wish #7093 (definitions link to themselves).
Hugo Herbelin
2020-04-20
TIMEFMT: Display the output file name
Jason Gross
2020-04-20
Merge PR #12091: Adding highlighting of the target of a internal link in defa...
Lysxia
2020-04-20
Adding change log.
Hugo Herbelin
2020-04-20
Adding highlighting of the target of a internal link in coqdoc CSS.
Hugo Herbelin
2020-04-20
Move new iter_table function to Goptions.
Théo Zimmermann
2020-04-20
Use polymorphic record for Vernacentries.iter_table
Gaëtan Gilbert
2020-04-20
Improve undeclared key messages.
Théo Zimmermann
2020-04-20
Merge PR #12123: Don't create index entries for the name "_"
Théo Zimmermann
2020-04-20
Merge PR #12125: Fix Makefile warning: undefined variable '*'
Gaëtan Gilbert
2020-04-20
Change log for PR #12045.
Hugo Herbelin
2020-04-20
Fixing #12045 (missing normalization in conclusion of custom induction scheme).
Hugo Herbelin
2020-04-20
Merge PR #12106: Coqide: Apply style scheme and language settings to the thre...
Pierre-Marie Pédrot
2020-04-20
Merge PR #12077: Update .mailmap
Théo Zimmermann
2020-04-19
Merge PR #12074: added changelog for PR 12044
Jason Gross
2020-04-19
added changelog for PR 12044
ilya
2020-04-19
Update .mailmap
Jason Gross
2020-04-19
Fix Makefile warning: undefined variable '*'
Jason Gross
2020-04-19
Don't create index entries for the name "_"
Jim Fehrle
2020-04-19
Merge PR #12033: Let coqdoc be informed by coq about binding variables (incid...
Lysxia
2020-04-19
CoqIDE: Adding a short documentation on style/theme customization.
Hugo Herbelin
2020-04-17
Coqide: Apply style scheme and language to the three buffers.
Hugo Herbelin
2020-04-17
Merge PR #12111: CI: Ignore spurious errors in validate jobs
Théo Zimmermann
2020-04-17
Merge PR #11976: Deprecate the omega tactic
Théo Zimmermann
2020-04-17
Merge PR #12112: Adapt linter documentation to the recent improvements of the...
Gaëtan Gilbert
2020-04-17
Adapt linter documentation to the recent improvements of the pre-commit hook.
Théo Zimmermann
2020-04-17
Deprecate “omega”
Vincent Laporte
2020-04-17
CI: Ignore spurious errors in validate jobs
Gaëtan Gilbert
2020-04-17
ZArith: move lia hints to a dedicated module
Vincent Laporte
2020-04-17
Merge PR #11963: NativeCompute Timing: Use real, not user time
Pierre-Marie Pédrot
2020-04-17
Merge PR #11135: Simplifying the code declaring the constants bound to primit...
Pierre-Marie Pédrot
2020-04-17
Merge PR #11972: Fix require in section
Pierre-Marie Pédrot
2020-04-16
NativeCompute Timing: Use real, not user time
Jason Gross
2020-04-16
Merge PR #12070: Ignore -native-compiler option when disabled
Pierre-Marie Pédrot
2020-04-16
Merge PR #11861: [declare] [rewrite] Use high-level declare API
Pierre-Marie Pédrot
2020-04-16
Merge PR #12069: [gitlab-ci] Only run Windows jobs when ONLY_WINDOWS variable...
Gaëtan Gilbert
2020-04-16
Merge PR #11982: Fix #11854 error message on unsolved evars in Instance.
Pierre-Marie Pédrot
2020-04-16
Merge PR #12101: Add needed commas in message
Gaëtan Gilbert
2020-04-16
Merge PR #11999: [proof] Merge `Proof_global` into `Declare`
Gaëtan Gilbert
2020-04-15
Add needed commas in message
Jim Fehrle
2020-04-15
Adding change log for PR #12033 (hyperlinks on binders for coqdoc).
Hugo Herbelin
2020-04-15
Coqdoc: Exporting location and unique id for binding variables.
Hugo Herbelin
2020-04-15
Making type interning_data abstract in constrintern.ml.
Hugo Herbelin
[next]