coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove duplicate lemmas.	Guillaume Melquiond	2017-03-22
*	Micromega: removing a constant preventing micromega to be loaded before Logic.v.	Hugo Herbelin	2017-03-09
*	Lazily load constants in micromega (bug #5134).	Guillaume Melquiond	2016-11-24
*	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
*	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
*	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\|\
* \|	Fixed Bug #5003 : more careful generalisation of dependent terms.	Frédéric Besson	2016-09-01
* \|	plugin micromega : nra also handles non-linear rational arithmetic over Q (Fi...	Frédéric Besson	2016-08-30
\| *	micromega cache files are now hidden files (cf #4156)	Frédéric Besson	2016-08-30
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	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