coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
*	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14
*	Tactics API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Retyping API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Reductionops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Termops API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
*	Make the Coq codebase independent from Ltac-related code.	Pierre-Marie Pédrot	2016-09-16
\|\
\| *	Moving Ltac-specific generic arguments to their own file in the ltac/ folder.	Pierre-Marie Pédrot	2016-09-15
* \|	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
* \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
* \|	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
* \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
* \|	Revert "Merge remote-tracking branch 'github/pr/229' into trunk"	Maxime Dénès	2016-07-05
* \|	Merge remote-tracking branch 'github/pr/229' into trunk	Maxime Dénès	2016-07-04
\|\ \
* \| \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
\| * \|	Makefile: no bytecode compilation in make world, see make byte instead	Pierre Letouzey	2016-06-29
\|/ /
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Compilation via pack for plugins of the stdlib	Pierre Letouzey	2016-06-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\\|
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
\| *	Disable memoization rather than failing when files cannot be opened.	Guillaume Melquiond	2016-05-20
* \|	Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/...	Pierre Letouzey	2016-05-19
* \|	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
* \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
* \|	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
* \|	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
* \|	Fix typos.	Guillaume Melquiond	2016-01-01
* \|	Changing the toplevel type of the int_or_var generic type to int.	Pierre-Marie Pédrot	2015-12-21
* \|	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
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-15
\|\\|
\| *	Fix some typos.	Guillaume Melquiond	2015-10-13
* \|	micromega : fix silly timeout	Frédéric Besson	2015-06-06
* \|	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
\|/
*	Fix some typos.	Guillaume Melquiond	2015-04-02
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09