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-02-08
Remove spaces just before period (non-math mode).
Tanaka Akira
2019-02-08
Remove spaces just before comma (non-math mode).
Tanaka Akira
2019-02-08
Remove "'" accidentaly added.
Tanaka Akira
2019-02-06
Merge PR #9124: Document the possibility of declaring a Ltac name_goal.
Clément Pit-Claudel
2019-02-06
Merge PR #9456: The lowest universe level is 1.
Théo Zimmermann
2019-02-06
Document the possibility of declaring a Ltac name_goal.
Théo Zimmermann
2019-02-06
Merge PR #9487: Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.
Enrico Tassi
2019-02-06
Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.
Théo Zimmermann
2019-02-05
Merge PR #9397: Simplify code for Recordops.cs_pattern_of_constr
Matthieu Sozeau
2019-02-05
Merge PR #9472: Add advice and an example to the documentation of fold.
Clément Pit-Claudel
2019-02-05
Merge PR #9373: Kernel: don't automatically downgrade ill-shaped primitive re...
Pierre-Marie Pédrot
2019-02-05
Merge PR #9438: Cleanup universe length for inductives in vconv
Pierre-Marie Pédrot
2019-02-05
Merge PR #9396: Skip indirection through Evd for obligation ustate manipulation
Matthieu Sozeau
2019-02-05
Merge PR #8421: [dune] Fix Dune build in Windows.
Théo Zimmermann
2019-02-05
Add advice and an example to the documentation of fold.
Théo Zimmermann
2019-02-04
Merge PR #9470: the default branch of Mtac2 changed to master
Emilio Jesus Gallego Arias
2019-02-04
Merge PR #9468: Remove AppVeyor: superseded by Azure.
Emilio Jesus Gallego Arias
2019-02-04
the default branch of Mtac2 changed to master
beta
2019-02-04
[dune] Fix Dune build in Windows.
Emilio Jesus Gallego Arias
2019-02-04
Remove AppVeyor: superseded by Azure.
Théo Zimmermann
2019-02-04
Merge PR #6914: Primitive integers
Pierre-Marie Pédrot
2019-02-04
Merge PR #9317: Restrict universes in records.
Pierre-Marie Pédrot
2019-02-04
Merge PR #9144: Fixes #4633: clearer message unknown existential
Pierre-Marie Pédrot
2019-02-04
Merge PR #9409: Move non-primitive-record warning to declare_mutual_inductive...
Pierre-Marie Pédrot
2019-02-04
Merge PR #9437: Comment universe operations in Classes.context
Pierre-Marie Pédrot
2019-02-04
Merge PR #9386: Pass some files to strict focusing mode.
Pierre-Marie Pédrot
2019-02-04
Overlays.
Maxime Dénès
2019-02-04
Primitive integers
Maxime Dénès
2019-02-04
Dockerfile: update menhir from 20180530 to 20181113
Vincent Laporte
2019-02-04
Merge PR #9368: Discard argument names of section variables on section close
Pierre-Marie Pédrot
2019-02-04
Merge PR #8690: [toplevel] Split interactive toplevel and compiler binaries.
Maxime Dénès
2019-02-04
Merge PR #9426: [test-suite] Fix display of check.
Enrico Tassi
2019-02-04
Merge PR #9454: Fix off-by-one error in nat syntax warnings
Pierre-Marie Pédrot
2019-02-04
Merge PR #9452: [proof] optimize proof always works on incomplete proofs
Pierre-Marie Pédrot
2019-02-04
Merge PR #9461: Fix default goal selector error message.
Pierre-Marie Pédrot
2019-02-04
Merge PR #9291: Do not take universes into account in lia reification.
Frédéric Besson
2019-02-02
Merge PR #9250: coqchk: fix check for kelim with functors
Pierre-Marie Pédrot
2019-02-02
Merge PR #9395: Global [open Univ] in UState
Pierre-Marie Pédrot
2019-02-01
Fix default goal selector error message.
Gaëtan Gilbert
2019-02-01
Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zify
Vincent Laporte
2019-02-01
[toplevel] Split interactive toplevel and compiler binaries.
Emilio Jesus Gallego Arias
2019-02-01
Merge PR #9415: Simplify the GitHub issue template
Maxime Dénès
2019-02-01
Merge PR #9095: [toplevel] Deprecate `-compile` flag in favor of `coqc`
Maxime Dénès
2019-02-01
The lowest universe level is 1.
Tanaka Akira
2019-01-31
Fix off-by-one error in nat syntax warnings
Jason Gross
2019-01-31
add test
Enrico Tassi
2019-01-31
[proof] optimize proof always works on incomplete proofs
Enrico Tassi
2019-01-31
Merge PR #9449: Fix small errors in cic.rst (2nd).
Théo Zimmermann
2019-01-31
Merge PR #9448: [ci] [ocaml] Fix OCaml trunk builds.
Gaëtan Gilbert
2019-01-31
Use λ instead of \lb.
Tanaka Akira
[next]