coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7897: Remove fourier plugin	Enrico Tassi	2018-07-18
\|\
\| *	Remove fourier plugin	Maxime Dénès	2018-07-17
* \|	[build] Build Coq and plugins with `-strict-sequence`	Emilio Jesus Gallego Arias	2018-07-14
\|/
*	Moving various ml4 files to mlg.	Pierre-Marie Pédrot	2018-07-02
*	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias	2018-06-12
*	Micromega clean-up	Maxime Dénès	2018-06-07
*	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
*	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert	2018-05-17
*	Deprecate undocumented "intros until 0" in favor of "intros *".	Hugo Herbelin	2018-03-23
*	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
*	[stdlib] Do not use “Require” inside sections	Vincent Laporte	2018-03-07
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	Merge PR #6234: Make the micromega extraction check a regular output test.	Maxime Dénès	2017-12-20
\|\
* \|	Replacing Hashtbl.add by Hashtbl.replace in micromega cache building.	Hugo Herbelin	2017-12-05
\| *	Make the micromega extraction check a regular output test.	Gaëtan Gilbert	2017-11-28
\|/
*	[printing] Deprecate all printing functions accessing the global proof.	Emilio Jesus Gallego Arias	2017-11-21
*	Fix micromega.ml to match generated file and enforce match in make.	Gaëtan Gilbert	2017-11-16
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms.	Emilio Jesus Gallego Arias	2017-10-05
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	Prelude : no more autoload of plugins extraction and recdef	Pierre Letouzey	2017-06-14
*	Makefile.build : cleanup now that micromega.ml isn't generated + sync check o...	Pierre Letouzey	2017-06-14
*	Store plugins/micromega/micromega.{ml,mli} files in the repository. Try to ge...	Matej Košík	2017-06-12
*	Merge PR#709: Bytecode compilation apart from 'make world', again	Maxime Dénès	2017-06-12
\|\
* \	Merge PR#718: API cleanup: aliases	Maxime Dénès	2017-06-12
\|\ \
* \| \|	Remove remaining vo.itarget files (obsolete since PR #499)	Pierre Letouzey	2017-06-10
\| * \|	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
* \|	Break circular dependency in MExtraction	Jason Gross	2017-06-01
* \|	extract "plugins/micromega/micromega.ml{,i}" files from "plugins/micromega/ME...	Matej Kosik	2017-06-01
\| *	Makefile: no bytecode compilation in make world, see make byte instead	Pierre Letouzey	2017-05-30
\|/
*	[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
\| *	Micromega: do not use Filename.temp_dir_path, remove unused values	Gaetan Gilbert	2017-04-27
\| *	Rename Sos_lib.(\|\|) -> parser_or to avoid (deprecated) Pervasives.or	Gaetan Gilbert	2017-04-27
\| *	Disambiguate Polynomial.Hyp and Mfourier.Hyp -> Assum	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
\| *	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
* \|	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\|\\|