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-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
2019-06-08
Merge PR #10318: Test goal range in "only" selectors
Pierre-Marie Pédrot
2019-06-08
Merge PR #10263: [proofs] Remove unused API [detected by coverage]
Pierre-Marie Pédrot
2019-06-08
Fix #10339: Anomaly in Ltac2.
Pierre-Marie Pédrot
2019-06-08
[Test-suite] Add non-regression test case for #8725
Vincent Laporte
2019-06-08
Overlays for Elpi + Equations + Mtac2 + fiat parsers + paramcoq.
Hugo Herbelin
2019-06-08
Cleaning the status of Local Definition and similar.
Hugo Herbelin
2019-06-08
Adding a new kind of assumption to track assumption coming from "Context".
Hugo Herbelin
2019-06-08
Test goal range in "only" selectors
Gaëtan Gilbert
2019-06-08
Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...
Pierre-Marie Pédrot
2019-06-08
Updated changelog.
Hugo Herbelin
2019-06-08
Mini fix documentation coqtop in passing.
Hugo Herbelin
2019-06-08
Documenting new options -require-import, -require-export, etc.
Hugo Herbelin
2019-06-08
Command line: adding variants for Require, aligning on the vernac syntax.
Hugo Herbelin
2019-06-07
Merge PR #10236: Update coqdev-setup-proofgeneral for dune
Emilio Jesus Gallego Arias
2019-06-07
Merge PR #10330: Dune: run coqc with -w +default
Emilio Jesus Gallego Arias
2019-06-07
Merge PR #10335: simple IO CI branch is now `master`
Emilio Jesus Gallego Arias
2019-06-07
Merge PR #10311: Ltac2 codeowner / changelog
Maxime Dénès
2019-06-07
simple IO CI branch is now `master`
Gaëtan Gilbert
2019-06-07
Merge PR #10308: Merge the two sources of monomorphic constraints for side-ef...
Gaëtan Gilbert
2019-06-07
test suite: don't try to coqchk failed tests
Gaëtan Gilbert
2019-06-07
Update changelog for 103032 and 10305
Enrico Tassi
2019-06-07
Dune: run coqc with -w +default
Gaëtan Gilbert
2019-06-07
Merge PR #10205: Make discriminate tactic compatible with HoTT
Pierre-Marie Pédrot
2019-06-07
Fix bug #5710
Claude Stolze
2019-06-06
Update doc/changelog/03-notations/10180-deprecate-notations.rst
Maxime Dénès
2019-06-06
Make discriminate tactic compatible with HoTT
Andreas Lynge
2019-06-06
Merge PR #10304: Clean up tuto0 and tuto1 to use better practices and explain...
Pierre-Marie Pédrot
2019-06-06
Merge PR #10278: vernac_load doesn't get a ?proof argument
Emilio Jesus Gallego Arias
2019-06-06
Merge PR #9972: [build] Select uint63 using `ocamlc -config` variables.
Vincent Laporte
2019-06-06
Doc for per commit compile lint
Gaëtan Gilbert
2019-06-06
CI: Test ml compilation of each commit in a PR in lint job
Gaëtan Gilbert
2019-06-06
Merge PR #10323: Remove old overlays
Emilio Jesus Gallego Arias
2019-06-06
Merge the two sources of monomorphic constraints for side-effects.
Pierre-Marie Pédrot
[prev]
[next]