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-30
Make the VM accumulator look like an OCaml block.
Pierre-Marie Pédrot
2018-04-30
Wrap VM bytecode used on the OCaml side in an OCaml block.
Pierre-Marie Pédrot
2018-04-30
Merge PR #6944: Strict focusing using Default Goal Selector.
Pierre-Marie Pédrot
2018-04-30
Merge PR #7355: [owners] Makefile.ci belongs to the CI category.
Maxime Dénès
2018-04-30
Merge PR #6958: [lib] Move global options to their proper place.
Maxime Dénès
2018-04-30
Merge PR #7381: [gitlab] Update base image to Ubuntu bionic + some improvements.
Gaëtan Gilbert
2018-04-29
Strict focusing using Default Goal Selector.
Gaëtan Gilbert
2018-04-29
tclSELECT: SelectAll never happens
Gaëtan Gilbert
2018-04-29
[gitlab] Update base image to Ubuntu bionic + some improvements.
Emilio Jesus Gallego Arias
2018-04-29
Merge PR #7386: [doc] Remove unused dependencies.
Théo Zimmermann
2018-04-28
[doc] Remove unused dependencies.
Emilio Jesus Gallego Arias
2018-04-28
Merge PR #7376: Fix gitlab ubuntu version
Emilio Jesus Gallego Arias
2018-04-28
Fix gitlab ubuntu version
Gaëtan Gilbert
2018-04-28
Merge PR #7357: [CI] elpi 1.0 has an official opam package
Emilio Jesus Gallego Arias
2018-04-28
Merge PR #7367: circle CI: do not use cache from old config.yml versions
Emilio Jesus Gallego Arias
2018-04-28
Merge PR #6892: Cleanup implementation of normalize_context_set a bit
Pierre-Marie Pédrot
2018-04-27
[CI] elpi 1.0 has an official opam package
Enrico Tassi
2018-04-27
circle CI: do not use cache from old config.yml versions
Gaëtan Gilbert
2018-04-27
Merge PR #7358: Fix #7356: missing lift when interpreting default instances o...
Enrico Tassi
2018-04-27
Merge PR #7351: Always print explanation for univ inconsistency, rm Flags.uni...
Emilio Jesus Gallego Arias
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
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
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
Merge PR #307: Adding a flag to support different naming modes for evar hypot...
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 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
[next]