index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2019-06-16
Overlays for Mtac2 and Equations.
Hugo Herbelin
2019-06-16
Turning "manual_implicits" into a list of position in impargs.ml.
Hugo Herbelin
2019-06-16
Adding location in warning telling implicit arguments differ in term and type.
Hugo Herbelin
2019-06-16
Merge PR #10327: Fix bug #5710
Pierre-Marie Pédrot
2019-06-16
Merge PR #10355: [funind] Untabify; necessary to ease the review of subsequen...
Pierre-Marie Pédrot
2019-06-16
- added OCaml copyright header to List.v (if for no other reason than out of ...
Michael Soegtrop
2019-06-15
Merge PR #10040: Install byte version of coqidetop.
Emilio Jesus Gallego Arias
2019-06-15
[dune] Install .byte version of coqidetop like for coqtop.
Théo Zimmermann
2019-06-15
Merge PR #10377: Rename expr and tacexpr tokens into ltac_expr token family.
Clément Pit-Claudel
2019-06-15
Rename expr and tacexpr tokens into ltac_expr token family.
Théo Zimmermann
2019-06-14
Merge PR #10376: Add a comment documenting what fontsupport.py is.
Clément Pit-Claudel
2019-06-14
Add a comment documenting what fontsupport.py is.
Théo Zimmermann
2019-06-14
Merge PR #10322: Update changes.rst as a follow-up to #9743
Théo Zimmermann
2019-06-13
Merge PR #10374: Integrate 8.9.0 and 8.9.1 changelog entries.
Clément Pit-Claudel
2019-06-13
Merge PR #10373: Add missing changelog entry for #10360.
Clément Pit-Claudel
2019-06-13
Integrate 8.9.0 and 8.9.1 changelog entries.
Théo Zimmermann
2019-06-13
Add missing changelog entry for #10360.
Théo Zimmermann
2019-06-13
Update, expand, and document plugin tutorial 2
Talia Ringer
2019-06-13
Merge PR #10319: [STM] Only VtSideeff can be VtNow/VtLater
Enrico Tassi
2019-06-13
Merge PR #10360: Resolve #9885 CoqIDE does not work on Windows
Emilio Jesus Gallego Arias
2019-06-12
Merge PR #10310: Fix #10283: clearer dependency documentation for building Co...
Clément Pit-Claudel
2019-06-12
[funind] Untabify; necessary to ease the review of subsequent work.
Emilio Jesus Gallego Arias
2019-06-12
Merge PR #10358: [docker] update elpi to 1.3.1
Gaëtan Gilbert
2019-06-12
Remove dependency of native_compile on global env for symbols
Gaëtan Gilbert
2019-06-12
Merge PR #10329: Update changelog for 10302 and 10305
Théo Zimmermann
2019-06-12
Merge PR #10180: `deprecated` attribute support for notations and syntactic d...
Théo Zimmermann
2019-06-12
Fix #9455: avoid update_global_env when unchanged Global.universes()
Gaëtan Gilbert
2019-06-12
Merge PR #10334: Remove the side-effect role from the kernel.
Enrico Tassi
2019-06-11
overlay
Enrico Tassi
2019-06-11
Adding an overlay for Equations.
Pierre-Marie Pédrot
2019-06-11
Move the side-effect role out of Entries into Evd.
Pierre-Marie Pédrot
2019-06-11
Remove the side-effect role from the kernel.
Pierre-Marie Pédrot
2019-06-11
Merge PR #10354: [ci] [fiat-crypto] Enable more targets on Coq CI
Emilio Jesus Gallego Arias
2019-06-11
Resolve #9885 CoqIDE does not work on Windows
Michael Soegtrop
2019-06-11
Move type definition Nativecode.symbols to Nativevalues
Gaëtan Gilbert
2019-06-11
Overlays for 10319
Gaëtan Gilbert
2019-06-11
STM: encode in static types that vernac_when is only used when VtSideff
Gaëtan Gilbert
2019-06-11
Fix #10225 (Instance := {} accepts duplicate fields)
Gaëtan Gilbert
2019-06-11
Simplify implicit_quantifiers
Gaëtan Gilbert
2019-06-11
update elpi to 1.3.1
Enrico Tassi
2019-06-10
[ci] [fiat-crypto] Enable more targets on Coq CI
Jason Gross
2019-06-10
Merge PR #9566: [proof] Move proofs that have an associated constant to `Lemmas`
Pierre-Marie Pédrot
2019-06-09
Merge PR #10325: Fix panel behavior as requested by #10292
Pierre-Marie Pédrot
2019-06-09
[ci] Overlays for move_termination_routine_out
Emilio Jesus Gallego Arias
2019-06-09
[proof] Uniformize Proof_global API
Emilio Jesus Gallego Arias
2019-06-09
[save_proof] Make terminator API internal.
Emilio Jesus Gallego Arias
2019-06-09
[proof] Move proofs that have an associated constant to `Lemmas`
Emilio Jesus Gallego Arias
2019-06-09
Merge PR #8726: More robust treatment of the Discharge status
Pierre-Marie Pédrot
2019-06-09
Merge PR #10309: CI: Test ml compilation of each commit in a PR in lint job
Emilio Jesus Gallego Arias
2019-06-09
Merge PR #10245: Command line: adding variants for Require, aligning on the v...
Emilio Jesus Gallego Arias
[prev]
[next]