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-01-22
A few edits to the 8.11 section of the Changes chapter.
Théo Zimmermann
2020-01-22
Changelog for 8.11.0.
Théo Zimmermann
2020-01-22
Merge PR #11422: Fix #11421 computation of Set+2
Pierre-Marie Pédrot
2020-01-22
Fix #11421 computation of Set+2
Gaëtan Gilbert
2020-01-22
Merge PR #11433: [xml-protocol doc] Fix link to vscoq
Hugo Herbelin
2020-01-21
[xml-protocol doc] Fix link to vscoq
Ramkumar Ramachandra
2020-01-21
More portable C flags
Pierre Roux
2020-01-21
Merge PR #11425: Miscellaneous typos
Théo Zimmermann
2020-01-21
Merge PR #11431: [ci] Pin SF until they solve their CI issues.
Théo Zimmermann
2020-01-21
[ci] Pin SF until they solve their CI issues.
Emilio Jesus Gallego Arias
2020-01-21
Translating a comment from French to English.
Hugo Herbelin
2020-01-21
Typo in an anomaly message.
Hugo Herbelin
2020-01-21
Typo in a comment of univ.mli.
Hugo Herbelin
2020-01-21
Reference manual: Typos/English in chapter universe polymorphism.
Hugo Herbelin
2020-01-20
Merge PR #11411: Checker validation now performed over reified data
Gaëtan Gilbert
2020-01-20
Merge PR #11428: [mltop] Deprecate -load-ml options in anticipation of #11409
Pierre-Marie Pédrot
2020-01-20
[mltop] Deprecate -load-ml options in anticipation of #11409
Emilio Jesus Gallego Arias
2020-01-20
Dispatch code ownership of files in dev/doc.
Théo Zimmermann
2020-01-19
Merge PR #11406: [dune] [dbg] Add support for coqtop in dune-dbg
Gaëtan Gilbert
2020-01-19
Merge PR #11214: Add a script to pin CI developments.
Gaëtan Gilbert
2020-01-19
Merge PR #11368: Turn trailing implicit warning into an error
Hugo Herbelin
2020-01-19
Merge PR #11398: Fix issue #11396 : Rlist hides standard list constructors co...
Pierre-Marie Pédrot
2020-01-19
Merge PR #11348: Discharge inductive types without rechecking them
Pierre-Marie Pédrot
2020-01-19
Removing text saying XML is future of PG, adding explicitly vscoq as a user
Hugo Herbelin
2020-01-17
Merge PR #11413: [doc] [ltac2] Build Ltac2 documentation
Théo Zimmermann
2020-01-17
Merge PR #11410: [ci] [gitlab] Add `interruptible: true` to jobs.
Théo Zimmermann
2020-01-17
Add some more info to the maintainer doc.
Théo Zimmermann
2020-01-17
Fix issue #11396 : Rlist hides standard list constructors cons and nil
Michael Soegtrop
2020-01-17
[doc] [ltac2] Build Ltac2 documentation [make build system]
Emilio Jesus Gallego Arias
2020-01-17
[doc] [dune] [ltac2] Build Ltac2 documentation [dune build system]
Emilio Jesus Gallego Arias
2020-01-17
[dune] [dbg] Add support for coqtop in dune-dbg
Emilio Jesus Gallego Arias
2020-01-17
[ci] [gitlab] Add `interruptible: true` to jobs.
Emilio Jesus Gallego Arias
2020-01-17
Merge PR #11362: Lia bugfix 11191
Maxime Dénès
2020-01-17
Remove the CoqIDE "Revert all Buffers" command.
Pierre-Marie Pédrot
2020-01-17
Remove the Tactic menu from CoqIDE.
Pierre-Marie Pédrot
2020-01-16
Merge PR #11400: Use the GTK completion widget in CoqIDE
Emilio Jesus Gallego Arias
2020-01-16
Adding a changelog.
Pierre-Marie Pédrot
2020-01-16
Adding an option to change the autocompletion delay.
Pierre-Marie Pédrot
2020-01-16
Better handling of asynchronous completion.
Pierre-Marie Pédrot
2020-01-16
Hacking a completion widget based on the default GtkSourceView one.
Pierre-Marie Pédrot
2020-01-16
Move the per-architecture check of marshalled Uint63s to Values.
Pierre-Marie Pédrot
2020-01-16
Checker validation acts on object representations rather than objects.
Pierre-Marie Pédrot
2020-01-16
Code factorization in checker validation.
Pierre-Marie Pédrot
2020-01-16
[mltop] Remove error handling hacks in favor of default methods.
Emilio Jesus Gallego Arias
2020-01-16
[mltop] Store digest of modules used to compile files.
Emilio Jesus Gallego Arias
2020-01-15
Merge PR #11373: Close #11168
Pierre-Marie Pédrot
2020-01-15
Merge PR #11374: Close #11133
Pierre-Marie Pédrot
2020-01-15
[ocaml] Remove Custom Backtrace module in favor of OCaml's
Emilio Jesus Gallego Arias
2020-01-15
Discharge inductive types without rechecking them
Gaëtan Gilbert
2020-01-15
generate variance data for section universes (not yet used)
Gaëtan Gilbert
[prev]
[next]