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-11
Notations: advertize that distinct "only parsing"/"only printing" rules work.
Hugo Herbelin
2018-05-11
Merge PR #7466: Remove tutorials from the repo
Maxime Dénès
2018-05-11
Merge PR #7461: [sphinx] Improve the proof handling chapter.
Maxime Dénès
2018-05-11
Merge PR #7341: Don't recurse into closed modules/sections in split_lib.
Enrico Tassi
2018-05-11
coqdev.el: add bug-reference-mode variables
Gaëtan Gilbert
2018-05-11
set_solve_evars doesn't use an evar_map ref
Gaëtan Gilbert
2018-05-11
Deprecate Evarconv.e_conv,e_cumul
Gaëtan Gilbert
2018-05-11
Convert clear_hyps_in_evi to state passing style.
Gaëtan Gilbert
2018-05-11
Deprecate most evarutil evdref functions
Gaëtan Gilbert
2018-05-11
Merge PR #7363: [ci] Fix another issue with the timing tests
Gaëtan Gilbert
2018-05-11
Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -o
Théo Zimmermann
2018-05-11
Remove packaging jobs from appveyor
Maxime Dénès
2018-05-11
Windows packaging build with Gitlab CI
Maxime Dénès
2018-05-10
Merge PR #7437: [coqdep] Minor cleanups.
Pierre-Marie Pédrot
2018-05-10
Suggest going to /documentation to see a list of tutorials.
Théo Zimmermann
2018-05-10
One can build all the HTML doc using default.nix.
Théo Zimmermann
2018-05-10
Clean-up in Makefile.doc and include Sphinx in doc-html target.
Théo Zimmermann
2018-05-10
Remove tutorials.
Théo Zimmermann
2018-05-10
Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).
Hugo Herbelin
2018-05-10
Fixes part 1 of #7462 (only-printing not to override existing interp rule).
Hugo Herbelin
2018-05-10
Merge PR #7473: [ci] Add mit-plv/cross-crypto
Emilio Jesus Gallego Arias
2018-05-10
Merge PR #7471: [travis] Fix version of camlp5 for OCaml 4.06.1.
Emilio Jesus Gallego Arias
2018-05-10
[build] Build checker generated files using a make rule.
Emilio Jesus Gallego Arias
2018-05-09
[ci] Add mit-plv/cross-crypto
Jason Gross
2018-05-09
[sphinx] Improve proof handling chapter.
Théo Zimmermann
2018-05-09
Clarify that the description of coqtop does not reflect all user interfaces.
Théo Zimmermann
2018-05-09
[sphinx] Improvements around the Show commands, including missing indices and...
Théo Zimmermann
2018-05-09
[travis] Add explicit opam switch command to guarantee we're using the reques...
Théo Zimmermann
2018-05-09
[travis] Fix version of camlp5 for OCaml 4.06.1.
Théo Zimmermann
2018-05-09
use at least 6 Xs in mktemp filename templates
Sven M. Hallberg
2018-05-09
test for coqc -o
Enrico Tassi
2018-05-09
Merge PR #7438: [gitlab] Do expensive builds with the flambda compiled Coq.
Gaëtan Gilbert
2018-05-09
Merge PR #7435: [gitlab] Add bleeding-edge flambda build.
Gaëtan Gilbert
2018-05-09
[sphinx] Warn for dangling tacn / cmd / opt / ... references.
Clément Pit-Claudel
2018-05-09
[sphinx] Fix new warnings related to tacn, cmd, opt...
Théo Zimmermann
2018-05-09
Replacing a broken reference by hyperlinks in chapter tactics.
Hugo Herbelin
2018-05-09
A few fixes in chapter tactics.
Hugo Herbelin
2018-05-08
Merge PR #7459: Try to fix CODEOWNERS
Théo Zimmermann
2018-05-08
Don't use ref universe_opt_subst
Gaëtan Gilbert
2018-05-08
Merge PR #7446: [lib] Re-add `set_timeout` to help users workaround #7408
Pierre-Marie Pédrot
2018-05-08
Try to fix CODEOWNERS
Maxime Dénès
2018-05-08
[gitlab] Do expensive builds with a flambda-compiled Coq.
Emilio Jesus Gallego Arias
2018-05-08
[api] Move universe syntax to `Glob_term`
Emilio Jesus Gallego Arias
2018-05-08
[CoqProject] Add some comments and remove unnecessary use of Pp.
Emilio Jesus Gallego Arias
2018-05-08
[coqdep] Remove unnecessary dependency on Pp and CError.
Emilio Jesus Gallego Arias
2018-05-08
[coqdep] Minor cleanups.
Emilio Jesus Gallego Arias
2018-05-08
[toplevel] Don't ignore output filename provided by user in -o
Emilio Jesus Gallego Arias
2018-05-07
[gitlab] Add bleeding-edge flambda build.
Emilio Jesus Gallego Arias
2018-05-07
[lib] Re-add `set_timeout` to help users workaround #7408
Emilio Jesus Gallego Arias
2018-05-07
[vernac] taint two out-of-api `to_constr` use in `comDefinition`.
Emilio Jesus Gallego Arias
[prev]
[next]