coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	Put the "generalize" tactic in the monad.	Pierre-Marie Pédrot	2016-05-16
*	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
*	Bugfix micromega: more careful syntaxification of terms of the form (Rinv t)	Frédéric Besson	2016-04-18
*	Renaming functions in Typing to stick to the standard e_* scheme.	Pierre-Marie Pédrot	2016-02-15
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Preventing an unwanted warning 5 "this function application is partial"	Hugo Herbelin	2015-11-07
* \|	Indexing Proofview.goals with a stage.	Pierre-Marie Pédrot	2015-10-20
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
* \|	micromega : options to limit proof search	Frédéric Besson	2015-05-26
* \|	Merge v8.5 into trunk	Hugo Herbelin	2015-05-15
\|\\|
* \|	maintenance micromega plugin	Frédéric Besson	2015-04-28
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.	Hugo Herbelin	2014-12-07
*	Writing the raw introduction tactic in the new monad.	Pierre-Marie Pédrot	2014-11-05
*	Compatibility for compilation with ocaml 3.12 (at least).	Hugo Herbelin	2014-08-01
*	micromega : improve efficiency/termination of type-checking	Frédéric Besson	2014-08-01
*	micromega : refification recognises @eq T for T convertible with Z or R	Frédéric Besson	2014-07-31
*	Fix semantics of change p with c to typecheck c at each specific occurrence o...	Matthieu Sozeau	2014-06-23
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	Fixing some generic equalities in Micromega.	Pierre-Marie Pédrot	2014-03-03
*	bugfix micromega: solved an ambiguous symbol resolution	fbesson	2013-11-15
*	Misc changes around coqtop.ml :	letouzey	2013-08-22
*	Restrict (try...with...) to avoid catching critical exn (part 11)	letouzey	2013-03-13
*	Modulification of identifier	ppedrot	2012-12-14
*	Ensure that a function declared with a label is used with it	letouzey	2012-12-08
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia	2012-09-14
*	Updating headers.	herbelin	2012-08-08
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	More cleaning	ppedrot	2012-06-01
*	lib directory is cut in 2 cma.	pboutill	2012-04-12
*	coq_micromega.ml: fix order of recursive calls to rconstant	glondu	2012-01-14
*	More newlines in debugging output of psatzl	glondu	2012-01-14
*	Coq_micromega: generic = on constr replaced by eq_constr	puech	2011-07-29
*	Q2R -> IQR	fbesson	2011-05-25
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...	fbesson	2011-05-23
*	added support to handle division by a constant over R	fbesson	2011-05-20
*	apply zeta reduction before syntaxification	fbesson	2011-05-18
*	Improved lia + experimental nlia	fbesson	2011-05-09
*	Definitions of positive, N, Z moved in Numbers/BinNums.v	letouzey	2011-05-05
*	Solve name conflict about pow introduced by commit 13546.	letouzey	2010-10-21
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	Modify the test for csdp and associated message.	fkirchne	2010-05-28
*	...	fkirchne	2010-05-28
*	Look for csdp in $PATH at runtime, remove -csdpdir configure option	glondu	2010-04-11
*	Application des patches envoyés par F. Besson pour micromega	notin	2010-03-08
*	OrderedType implementation for various numerical datatypes + min/max structures	letouzey	2009-11-03