coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing the convenience functions from the Search API.	Pierre-Marie Pédrot	2016-06-07
*	avoid communicating to the serarch interface using raw strings.	Gregory Malecha	2016-04-24
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	search: Add an output-name-only search option	Clément Pit--Claudel	2015-07-27
\|/
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Make native compiler handle universe polymorphic definitions.	Maxime Dénès	2015-01-17
*	Update headers.	Maxime Dénès	2015-01-12
*	Avoiding introducing yet another convention in naming files.	Hugo Herbelin	2015-01-08
*	Error messages of Searchxxx are coherent with goal selector.	Pierre Courtieu	2014-12-16
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Initial work on reintroducing old-style polymorphism for compatibility (the s...	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)	Pierre Letouzey	2014-03-02
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	Matching patterns: fixed allow_partial_app which was not working on	herbelin	2013-04-17
*	Exporting the SearchAbout filter.	ppedrot	2013-04-02
*	Removing the module Libtypes and unifying the Search[Pattern\|Rewrite]?	ppedrot	2013-03-19
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Names: revised representation of constants and mutual_inductive	letouzey	2013-02-19
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (toplevel)	ppedrot	2012-11-26
*	Added a CString module.	ppedrot	2012-11-13
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	When asked for a SearchAbout request, Coq now returns a more precise	ppedrot	2012-09-09
*	Updating headers.	herbelin	2012-08-08
*	Moved code out of ide_slave in a more appropriate place.	ppedrot	2012-07-09
*	Fixing test-suite after last storm in Pp.	pboutill	2012-06-12
*	Getting rid of Pp.msg	ppedrot	2012-05-30
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Noise for nothing	pboutill	2012-03-02
*	Various simplifications about constant_of_delta and mind_of_delta	letouzey	2011-10-11
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	Filter out admitted subgoals from search results	glondu	2011-02-25
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Fix function applications without labels (OCaml warning 6)	glondu	2010-09-28
*	Some dead code removal, thanks to Oug analyzer	letouzey	2010-09-24
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	Filter out "_subproof" objects from search results	puech	2010-03-11