coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
\| *	Removing tactic compatibility layer in Micromega.	Pierre-Marie Pédrot	2017-04-24
\|/
*	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\|\
\| *	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
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|
* \|	Micromega API using EConstr.	Pierre-Marie Pédrot	2017-02-14
* \|	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
\| *	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