index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
Age
Commit message (
Expand
)
Author
2018-04-26
Merge PR #7321: configure: make -annotate fatal, and color error and warnings
Emilio Jesus Gallego Arias
2018-04-26
Merge PR #7350: Updating CI to recent changes in Mtac2 (former MetaCoq)
Emilio Jesus Gallego Arias
2018-04-26
[ci] Fix another issue with the timing tests
Jason Gross
2018-04-26
Pretyping: Fixing a de Bruijn bug in interpreting default instances of evars.
Hugo Herbelin
2018-04-26
[owners] Makefile.ci belongs to the CI category.
Emilio Jesus Gallego Arias
2018-04-26
Add check-owners-pr.sh wrapper around check-owners
Gaëtan Gilbert
2018-04-26
[api] Move `hint_info_expr` to `Typeclasses`.
Emilio Jesus Gallego Arias
2018-04-26
Merge PR #7331: Fix a typo in the reference manual: <; -> <:
Maxime Dénès
2018-04-26
Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bit
Maxime Dénès
2018-04-26
Always print explanation for univ inconsistency, rm Flags.univ_print
Gaëtan Gilbert
2018-04-25
updating CI for Mtac2
Beta Ziliani
2018-04-25
Merge PR #7290: Update debugging.md
Hugo Herbelin
2018-04-25
Merge PR #6866: Slight improvement of messages related to direct and indirect...
Pierre-Marie Pédrot
2018-04-25
Merge PR #7322: Test suite Makefile: print message for failing tests as they ...
Enrico Tassi
2018-04-24
Don't recurse into closed modules/sections in split_lib.
Jasper Hugunin
2018-04-24
Remove DirClosedSection.
Jasper Hugunin
2018-04-24
Merge PR #307: Adding a flag to support different naming modes for evar hypot...
Pierre-Marie Pédrot
2018-04-24
Merge pull request coq/ltac2#50 from Armael/fix-typo
Pierre-Marie Pédrot
2018-04-24
Merge PR #6512: [api] Relocate `intf` modules according to dependency-order.
Pierre-Marie Pédrot
2018-04-24
Improving error message for clear tactic (and indirect uses of it).
Hugo Herbelin
2018-04-24
Adding a flag to support different naming modes for evar hypotheses.
Hugo Herbelin
2018-04-23
[api] Relocate `intf` modules according to dependency-order.
Emilio Jesus Gallego Arias
2018-04-23
Merge PR #7152: [api] Remove dependency of library on Vernacexpr.
Pierre-Marie Pédrot
2018-04-23
Merge PR #7108: Legacy refiner handle eta-expanded case analysis
Pierre-Marie Pédrot
2018-04-23
Merge PR #7244: Making tactic-in-term aware of "Set Ltac Debug"
Pierre-Marie Pédrot
2018-04-23
Merge PR #7240: [doc] [engine] Document `abort_on_undefined_evars`.
Pierre-Marie Pédrot
2018-04-23
Fix #7327: coqchk subtyping of polymorphic constants
Gaëtan Gilbert
2018-04-23
improve indentation
Enrico Tassi
2018-04-23
Fix a typo in the reference manual: <; -> <:
Kazuhiko Sakaguchi
2018-04-22
test suite: clean more things (glob, MExtraction.out, distclean aux)
Gaëtan Gilbert
2018-04-22
test suite: print message for failing tests as they come
Gaëtan Gilbert
2018-04-22
test suite Makefile: do not use %.stamp for subsystem targets
Gaëtan Gilbert
2018-04-22
configure: make -annotate fatal, and color error and warnings
Gaëtan Gilbert
2018-04-21
Merge PR #7320: [ci] Also make some display targets for fiat-crypto
Emilio Jesus Gallego Arias
2018-04-21
Merge PR #7319: CI: add fcsl-pcm
Emilio Jesus Gallego Arias
2018-04-20
[ci] Also make some display targets for fiat-crypto
Jason Gross
2018-04-20
CI: add fcsl-pcm
Anton Trunov
2018-04-20
Merge PR #6908: Move VM global tables from C to ML
Maxime Dénès
2018-04-20
Fix #6798: coqchk ignores ugraph when comparing constant instances
Gaëtan Gilbert
2018-04-19
Merge PR #7282: [toplevel] allow toploop_init change Coq options
Emilio Jesus Gallego Arias
2018-04-19
Merge PR #7219: merge script support https + typos in doc
Maxime Dénès
2018-04-19
Merge PR #7248: Assign circleci files to @SkySkimmer
Maxime Dénès
2018-04-19
Merge PR #7294: fix Iris ci
Emilio Jesus Gallego Arias
2018-04-19
[toplevel] let toploop_init change Coq options
Enrico Tassi
2018-04-19
Merge PR #7287: [default.nix] Build doc with nix-build.
Vincent Laporte
2018-04-19
Allowing formatting break around a printed type.
Hugo Herbelin
2018-04-19
Fixing printing level for subtypes of a type constructor.
Hugo Herbelin
2018-04-18
Merge PR #7281: [stm] push functional API further
Emilio Jesus Gallego Arias
2018-04-18
Merge PR #7280: [stm] expose restore/backup since ~doc is (still) dummy
Emilio Jesus Gallego Arias
2018-04-18
CI: extract iris git version without using opam
Ralf Jung
[prev]
[next]