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-05-02
Merge PR #7370: Fix PHONY typo in coq_makefile
Enrico Tassi
2018-05-01
Merge PR #7305: [toplevel] improve indentation
Emilio Jesus Gallego Arias
2018-05-01
Automatically run alienclean before compiling.
Gaëtan Gilbert
2018-05-01
Actually take advantage of the normalization status of kernel closures.
Pierre-Marie Pédrot
2018-05-01
ci-vst.sh: use -o progs
Gaëtan Gilbert
2018-05-01
Merge PR #7397: [ci] Fix #7396: VST is broken
Gaëtan Gilbert
2018-05-01
[ci] Fix #7396: VST is broken
Emilio Jesus Gallego Arias
2018-05-01
[api] Move bullets and goals selectors to `proofs/`
Emilio Jesus Gallego Arias
2018-04-30
[ci] [travis] Install num by default in all switches.
Emilio Jesus Gallego Arias
2018-04-30
Merge PR #7379: [doc] Update Sphinx build instructions for Debian derivatives.
Théo Zimmermann
2018-04-30
Merge PR #6935: Separate universe minimization and evar normalization functions
Pierre-Marie Pédrot
2018-04-30
Adapt the VM GC hook to handle the no-naked-pointers option flag.
Pierre-Marie Pédrot
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
[doc] Update Sphinx build instructions for Debian derivatives.
Emilio Jesus Gallego Arias
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
Fix the secondary maintainer for Makefile.
Théo Zimmermann
2018-04-29
Change maintainers for universe files in the kernel / engine.
Théo Zimmermann
2018-04-29
Implement to_constr with nf_evars_and_universes_opt_subst
Gaëtan Gilbert
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
Fix nf_evars_universes_opt_subst: recurse on univs, nf undef evars
Gaëtan Gilbert
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
Fix PHONY typo in coq_makefile
Gaëtan Gilbert
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
[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
[prev]
[next]