coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\
\| *	Prevent unsafe overwriting of Required modules by toplevel library.	Maxime Dénès	2016-07-05
\| *	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
* \|	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey	2016-07-03
* \|	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
* \|	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
* \|	A new infrastructure for warnings.	Maxime Dénès	2016-06-29
* \|	Shrink Proofs/Obligations by default and deprecate	Matthieu Sozeau	2016-06-27
* \|	[feedback] Add optional ?loc parameter to loggers.	Emilio Jesus Gallego Arias	2016-06-25
* \|	Fix bug #4825: [clear] should not dependency-check hypotheses that come above...	Pierre-Marie Pédrot	2016-06-20
* \|	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
* \|	Moving the typing_flags to the environment.	Pierre-Marie Pédrot	2016-06-18
* \|	Adding a local type-in-type flag in kernel declarations.	Pierre-Marie Pédrot	2016-06-18
* \|	Factorizing the uses of Declareops.safe_flags.	Pierre-Marie Pédrot	2016-06-16
* \|	Adding a default safe set of kernel typing flags to Declareops.	Pierre-Marie Pédrot	2016-06-16
* \|	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
\|\ \
\| * \|	Assume totality: dedicated type rather than bool	Arnaud Spiwack	2016-06-14
* \| \|	newring: fix for hack using evars as integers.	Matthieu Sozeau	2016-06-09
* \| \|	Adding a bit of documentation in the mli.	Pierre-Marie Pédrot	2016-06-09
* \| \|	Please never mention .mli-only file in .mllib (or future .mlpack)	Pierre Letouzey	2016-06-02
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-01
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Fix potential race condition in vm_compute.	Guillaume Melquiond	2016-05-31
* \| \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \| \|	Checker: avoid using obsolete names from Names	Pierre Letouzey	2016-05-31
\| * \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \| \|	native_compute: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \| \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-02
\|\\| \|
\| * \|	Fixing an incompatility introduced in a404360: kernel conversion was	Hugo Herbelin	2016-04-27
* \| \|	This is an attempt to clarify terminology in choosing variable names	Hugo Herbelin	2016-04-14
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-30
\|\\| \|
* \| \|	Remove int64 emulation in bytecode interpreter.	Maxime Dénès	2016-03-25
\| * \|	A patch renaming equal into eq in the module dealing with	Hugo Herbelin	2016-03-22
\| * \|	Adding eq/compare/hash for syntactic view at	Hugo Herbelin	2016-03-22
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-18
\|\\| \|
\| * \|	Primitive projections: protect kernel from erroneous definitions.	Matthieu Sozeau	2016-03-10
* \| \|	Removing OCaml deprecated function names from the Lazy module.	Pierre-Marie Pédrot	2016-03-10
\| * \|	Hashconsing modules.	Pierre-Marie Pédrot	2016-03-10
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\\| \|
\| * \|	This fix is probably not enough to justify that there are no problems with	Maxime Dénès	2016-03-04
\| * \|	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
* \| \|	ADD: Names.Name.is_{anonymous,name}	Matej Kosik	2016-02-18
* \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-17
\|\ \ \
* \| \| \|	Term: fix a comment (first de Bruijn index is 1)	Pierre Letouzey	2016-02-16
\| * \| \|	Renaming variants of Entries.local_entry	Matej Kosik	2016-02-16
\| * \| \|	CLEANUP: Simplifying the changes done in "kernel/*"	Matej Kosik	2016-02-15
\| * \| \|	REFORMATTING: kernel/context.ml{,i}	Matej Kosik	2016-02-09
\| * \| \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
\|/ / /
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\\| \|
\| * \|	Fixing bde12b70 about reporting ill-formed constructor.	Hugo Herbelin	2016-01-26