index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2021-04-14
Cleanup useless environment manipulation in Class declaration
Gaëtan Gilbert
2021-04-13
Merge PR #14024: [coqdep] error on non-existent and unreadable files
coqbot-app[bot]
2021-04-12
[coqdep] error on non-existent and unreadable files
Hendrik Tews
2021-04-12
Fix unknown -vos option for coqdep_boot introduced in PR #11074
Hendrik Tews
2021-04-12
Merge PR #14107: Gitignore update for doc_grammar and omega clean-up.
coqbot-app[bot]
2021-04-12
Remove omega from doc_grammar files.
Théo Zimmermann
2021-04-12
Gitignore update for doc_grammar.
Théo Zimmermann
2021-04-12
Merge PR #14038: [dune] [coqdoc] Install coqdoc.sty also in share/texmf
coqbot-app[bot]
2021-04-12
Merge PR #14061: [zify] better error reporting
Vincent Laporte
2021-04-12
Merge PR #14046: make critical sections safe in the presence of exceptions
coqbot-app[bot]
2021-04-12
[zify] better error reporting
BESSON Frederic
2021-04-10
Merge PR #14091: Fix link in doc/cic.rst, there is no Credits chapter anymore
coqbot-app[bot]
2021-04-10
Merge PR #13860: [coqrst] Show "Error:"/"Warning:" with white type (on red/or...
coqbot-app[bot]
2021-04-10
Fix link in doc/cic.rst, there is no Credits chapter anymore
Yannick Forster
2021-04-09
Make critical sections safe in the presence of exceptions
Lasse Blaauwbroek
2021-04-08
Merge PR #14065: Documenting some parts of gramlib/grammar.ml
coqbot-app[bot]
2021-04-08
Merge PR #14095: Fix a GTK warning in CoqIDE introduced by #14063.
coqbot-app[bot]
2021-04-08
Merge PR #14093: Register Ltac2 grammar entry as "ltac2" for the Print Gramma...
coqbot-app[bot]
2021-04-08
Gramlib: documentation of the recovery mechanism.
Hugo Herbelin
2021-04-08
Gramlib: some comments about how new rules are inserted.
Hugo Herbelin
2021-04-08
Gramlib: some comments about the main start/continue parsing loop.
Hugo Herbelin
2021-04-08
Merge PR #14080: CI-paramcoq: Re-enable native
coqbot-app[bot]
2021-04-08
Fix a GTK warning in CoqIDE introduced by #14063.
Pierre-Marie Pédrot
2021-04-08
Register Ltac2 grammar entry as "ltac2" for the Print Grammar vernacular.
Pierre-Marie Pédrot
2021-04-08
Merge PR #14027: Print type of offending expression in Ltac2 not-unit warning.
coqbot-app[bot]
2021-04-08
Merge PR #14062: Fixes #11690: wrongly toggled coqide printing matching flag
Pierre-Marie Pédrot
2021-04-07
Merge PR #14032: CI: don't output-sync
coqbot-app[bot]
2021-04-07
Merge PR #14078: Remove unused UnivProblem.Set.subst_univs
Pierre-Marie Pédrot
2021-04-07
Merge PR #14085: Dune: fix coqbyte shim after byterun->coqrun renaming
coqbot-app[bot]
2021-04-07
Dune: fix coqbyte shim after byterun->coqrun renaming
Gaëtan Gilbert
2021-04-07
Merge PR #14056: Miscellaneous mini-"typos" fixes
coqbot-app[bot]
2021-04-07
Merge PR #14008: [stdlib] [Arith] Cantor pairing
coqbot-app[bot]
2021-04-06
Merge PR #14077: Add odoc warnings for empty packages.
coqbot-app[bot]
2021-04-06
Add a relative link to coq-core.
Théo Zimmermann
2021-04-06
Typo in ChoiceFacts.
Hugo Herbelin
2021-04-06
Missing dot in an error message.
Hugo Herbelin
2021-04-06
One catch-all's missing a noncritical; another is now useless (see 7efaf86).
Hugo Herbelin
2021-04-06
Standardizing spacing for {| ... |} in two files.
Hugo Herbelin
2021-04-06
Typo in a micromega comment.
Hugo Herbelin
2021-04-06
Uniformizing the "already exists" messages
Hugo Herbelin
2021-04-06
Make description of Pp.pr_enum more precise + spacing in pp.ml.
Hugo Herbelin
2021-04-06
CI-paramcoq: Re-enable native
Gaëtan Gilbert
2021-04-06
Merge PR #13741: Remove omega tactic (deprecated in 8.12)
coqbot-app[bot]
2021-04-06
Add odoc warnings for empty packages.
Théo Zimmermann
2021-04-06
Remove unused UnivProblem.Set.subst_univs
Gaëtan Gilbert
2021-04-06
Merge PR #14042: Fix a bug in UnivProblem
Pierre-Marie Pédrot
2021-04-06
Merge PR #14063: Coqide: fixes #10720, highlight Variant keyword
Pierre-Marie Pédrot
2021-04-06
Merge PR #14069: [coqpp] Add -help
Pierre-Marie Pédrot
2021-04-05
Merge PR #13624: Fixing #13581: missing support for let-ins in arity of induc...
coqbot-app[bot]
2021-04-04
More extraction tests for inductive types with let-ins.
Hugo Herbelin
[next]