coq - The formal proof system

Age	Commit message (Expand)	Author
2019-07-08	[core] [api] Support OCaml 4.08	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-04-29	Revert #9249	Vincent Laporte
2018-12-25	Adding a comparison combinator for pairs.	Hugo Herbelin
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-09-12	Adding function to be typically used to pass values from an OCaml "when" clause.	Hugo Herbelin
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-05-19	Moving "sym" on "eq" type to lib/util.ml.	Hugo Herbelin
2016-08-30	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik
2016-03-13	Adding a few functions on type union.	Hugo Herbelin
2016-02-17	CLEANUP: Renaming "Util.compose" function to "%"	Matej Kosik
2016-01-21	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-12-05	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot
2015-07-28	Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)	Guillaume Melquiond
2015-01-12	Update headers.	Maxime Dénès
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-12-14	Util.un_op -> Option.default	Pierre Boutillier
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-11-19	Making map_union a standard function of the ML library.	Hugo Herbelin
2014-06-07	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot
2014-04-23	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot
2014-03-05	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot
2013-10-10	Clib: fold_left_until added to CList	gareuselesinge
2013-09-06	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot
2013-08-28	Removing some lone List.assoc & List.mem in lib.	ppedrot
2013-08-25	Added a more efficient way to recover the domain of a map.	ppedrot
2013-06-12	Changing the type of Ltac values. Now they are toplevel generic	ppedrot
2012-12-14	Moved Stringset and Stringmap to String namespace.	ppedrot
2012-12-14	Moved Intset and Intmap to Int namespace.	ppedrot
2012-11-13	Added a CString module.	ppedrot
2012-09-18	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey
2012-09-18	Cleaning interface of Util.	ppedrot
2012-09-17	More cleaning on Utils and CList. Some parts of the code being	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Added some tricky tail-rec versions of List functions to CList	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-08-08	Updating headers.	herbelin
2012-05-23	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill
2012-04-15	Adding newline after warning and restoring distinction between	herbelin
2012-03-26	Unification: Added a heuristic to solve problems of the form	herbelin
2012-03-20	Reorganizing the structure of evarutil.ml (only restructuration, no	herbelin
2012-03-18	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin
2012-03-14	Second step of integration of Program:	msozeau
2012-03-02	Noise for nothing	pboutill
2011-12-17	Added ability to take the type of applied metas into account when	herbelin
2011-11-28	Finally used typing to decide whether an alias needs to be expanded or	herbelin
2011-08-10	Added list_map_filter_i	msozeau
2011-07-29	Refl_omega: replaced some generic = on constr by eq_constr	puech