coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Util.Empty: implement using polymorphic record.	Gaëtan Gilbert	2018-07-03
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Adding function to be typically used to pass values from an OCaml "when" clause.	Hugo Herbelin	2017-09-12
*	Moving "sym" on "eq" type to lib/util.ml.	Hugo Herbelin	2017-05-19
*	[safe-string] lib/miscelanea	Emilio Jesus Gallego Arias	2017-03-14
*	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
*	Cleaning unpolished commit 0dfd0fb7d7 on basic functions about union type.	Hugo Herbelin	2016-04-15
*	Adding a few functions on type union.	Hugo Herbelin	2016-03-13
*	CLEANUP: Renaming "Util.compose" function to "%"	Matej Kosik	2016-02-17
*	Leveraging GADTs to provide a better Dyn API.	Pierre-Marie Pédrot	2015-12-05
*	Use open_utf8_file_in for opening files in the IDE. (Fix bug #2874)	Guillaume Melquiond	2015-07-28
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Util.un_op -> Option.default	Pierre Boutillier	2014-12-14
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Making map_union a standard function of the ML library.	Hugo Herbelin	2014-11-19
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot	2014-03-05
*	Allocation friendly version of Util.iterate.	ppedrot	2013-11-04
*	Clib: fold_left_until added to CList	gareuselesinge	2013-10-10
*	Removing a bunch of generic equalities.	ppedrot	2013-09-27
*	Get rid of the uses of deprecated OCaml elements (still remaining compatible ...	xclerc	2013-09-19
*	Moving Searchstack to CStack, and normalizing names a bit.	ppedrot	2013-09-06
*	Removing some lone List.assoc & List.mem in lib.	ppedrot	2013-08-28
*	Added a more efficient way to recover the domain of a map.	ppedrot	2013-08-25
*	Changing the type of Ltac values. Now they are toplevel generic	ppedrot	2013-06-12
*	Moved Stringset and Stringmap to String namespace.	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	More monomorphizations	ppedrot	2012-11-13
*	Added a CString module.	ppedrot	2012-11-13
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	Removed many calls to OCaml generic equality. This was done by	ppedrot	2012-10-29
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	More cleanup of Util: utf8 aspects moved to a new file unicode.ml	letouzey	2012-09-18
*	Cleaning interface of Util.	ppedrot	2012-09-18
*	More cleaning on Utils and CList. Some parts of the code being	ppedrot	2012-09-17
*	Some documentation and cleaning of CList and Util interfaces.	ppedrot	2012-09-15
*	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-09-14
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Revert copy/pasted function in to minilib thanks to clib.cma	pboutill	2012-05-23
*	Adding newline after warning and restoring distinction between	herbelin	2012-04-15
*	Shortcuts and optimizations of comparisons	xclerc	2012-04-05
*	Unification: Added a heuristic to solve problems of the form	herbelin	2012-03-26
*	Reorganizing the structure of evarutil.ml (only restructuration, no	herbelin	2012-03-20
*	Yet another subtlety with bug 2732: when several grammar rules of a	herbelin	2012-03-18
*	Second step of integration of Program:	msozeau	2012-03-14
*	Noise for nothing	pboutill	2012-03-02
*	Added ability to take the type of applied metas into account when	herbelin	2011-12-17