coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Properly compute types for assumed section variables (bug #5035).	Guillaume Melquiond	2016-08-24
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot	2016-06-18
*	Print the type-in-type flag in various user-facing functions.	Pierre-Marie Pédrot	2016-06-18
*	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot	2016-06-16
*	Merging "https://github.com/coq/coq/pull/94", i.e. "Traversal of inductive de...	Matej Kosik	2016-04-04
\|\
* \|	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
\|/ /
* \|	Print Assumptions: improve detection of case on an axiom of False	Enrico Tassi	2015-12-09
* \|	Fix #3948 Anomaly: unknown constant in Print Assumptions	Maxime Dénès	2015-09-20
* \|	Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on.	Pierre-Marie Pédrot	2015-09-15
\| *	Traversal of inductive defs in Print Assumptions	mlasson	2015-07-27
\|/
*	Fix loop in assumptions (Close: #4275)	Enrico Tassi	2015-07-02
*	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	2015-06-29