coq - The formal proof system

Age	Commit message (Expand)	Author
2017-12-11	Remove deprecated appcontext and corresponding documentation.	Théo Zimmermann
2017-12-10	[make] remove unneeded generated file "tolink.ml"	Emilio Jesus Gallego Arias
2017-12-10	[build] Remove coqmktop in favor of ocamlfind.	Emilio Jesus Gallego Arias
2017-12-07	Merge PR #6277: Qualified import in coqchk	Maxime Dénès
2017-12-05	use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language	Paul Steckler
2017-12-05	Merge PR #890: Global universe declarations	Maxime Dénès
2017-12-05	Merge PR #6300: Clarify operation of sequences, fixes #6095	Maxime Dénès
2017-12-05	Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212	Maxime Dénès
2017-12-01	clarify operation of sequences, #6095	Paul Steckler
2017-12-01	[refman] Expand a little on global universes.	Matthieu Sozeau
2017-12-01	Documenting the -Q flag of coqchk.	Pierre-Marie Pédrot
2017-12-01	Merge PR #6276: Coqchk accepts filenames	Maxime Dénès
2017-11-29	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot
2017-11-28	use \ocaml macro in new text	Paul Steckler
2017-11-28	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert
2017-11-25	Allow local universe renaming in Print.	Gaëtan Gilbert
2017-11-22	use OCaml criteria for infix ops, #6212	Paul Steckler
2017-11-19	Rename coq-inferior.el -> inferior-coq.el to match provided feature.	Gaëtan Gilbert
2017-11-13	coq_makefile: document COQ_SRC_SUBDIRS	Enrico Tassi
2017-11-06	Documentation: "tac1 \|\| tac2" means "first [ progress tac1 \| tac2 ]",	Samuel Gruetter
2017-11-06	Merge PR #1139: Add a linter.	Maxime Dénès
2017-10-27	Merge PR #6005: Fixes to documentation, addressed #4846, #5413 and #5631	Maxime Dénès
2017-10-25	Rename \Tree to \NatTree	Johannes Kloos
2017-10-25	Put newlines at the end of files.	Gaëtan Gilbert
2017-10-24	Fix #5763: Strictly positive example is out of order.	jkloos
2017-10-24	Fix #4846	Johannes Kloos
2017-10-24	Fix #5413: [unfold ... in] not documented	Johannes Kloos
2017-10-24	Documentation: Add various basic constructs to the index.	Johannes Kloos
2017-10-24	Fix part of 'Hard to find documentation for `(...) and `{...} #5631'	Johannes Kloos
2017-10-11	Remove GeoProof support.	Maxime Dénès
2017-10-05	Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...	Maxime Dénès
2017-10-03	Merge PR #1080: Remove some unused parts of the reference manual.	Maxime Dénès
2017-09-29	[vernac] Remove `Qed exporting` syntax.	Emilio Jesus Gallego Arias
2017-09-22	Remove some unused parts of the reference manual.	Guillaume Melquiond
2017-09-22	Avoid generated names for html pages of the reference manual (bug #4742).	Guillaume Melquiond
2017-09-13	Reference manual: A few words about the file system constraints for -Q/-R.	Hugo Herbelin
2017-09-11	Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`	Maxime Dénès
2017-09-11	Merge PR #1035: Fix the introduction of SSR refman chapter.	Maxime Dénès
2017-09-11	Merge PR #1014: Add option index entry for NativeCompute Profiling	Maxime Dénès
2017-09-11	Merge PR #1004: Document primitive projections in more detail	Maxime Dénès
2017-09-08	Fix Typo in Doc for `Set Parsing Explicit`	staffehn
2017-09-08	Fix the introduction of SSR refman chapter.	Théo Zimmermann
2017-09-03	2 Typos in 'Add Parametric Morphism' Documentation	staffehn
2017-09-01	add option index entry for NativeCompute Profiling	Paul Steckler
2017-09-01	Fixing various typos in the Credits chapter.	Théo Zimmermann
2017-08-31	Document primitive projections in more detail	Matthieu Sozeau
2017-08-31	RefMan-ssr: fix warning	Matthieu Sozeau
2017-08-31	Merge PR #993: Credits for version 8.7	Maxime Dénès
2017-08-31	Credits for version 8.7	Matthieu Sozeau
2017-08-31	Merge PR #958: coq_makefile: build/use .cma for packed plugins too	Maxime Dénès