coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \|	Extraction: fix complexity issue #5310	Pierre Letouzey	2017-02-07
\|/ / /
\| \| *	Extraction: fix complexity issue #5310	Pierre Letouzey	2017-02-07
\| * \|	Remove useless comments	Gaetan Gilbert	2017-01-28
\| * \|	Extend Fast_typeops to be a replacement for Typeops	Gaetan Gilbert	2016-12-12
\|/ /
* \|	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik	2016-10-19
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-17
\|\\|
\| *	Fix bug #5023: JSON extraction doesn't generate "for xxx".	Pierre-Marie Pédrot	2016-10-17
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\|
\| *	Extraction: ignore some useless stuff about universes	Pierre Letouzey	2016-09-29
* \|	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot	2016-09-21
* \|	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
* \|	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
\|/
*	Make it a bit more obvious when variables are of type unit.	Guillaume Melquiond	2016-08-10
*	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
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-06-27
\|\
\| *	Fix typo.	Guillaume Melquiond	2016-06-23
* \|	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
\| *	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
* \|	Extraction : add a location in the error message about polyprop	Pierre Letouzey	2016-05-30
\| *	Extraction/Projections: Fix bug #4710	Matthieu Sozeau	2016-05-23
* \|	Extraction: code cleanup in Common	Pierre Letouzey	2016-05-20
\| *	Extraction: don't call Unicode.ascii_of_ident twice (not idempotent anymore)	Pierre Letouzey	2016-05-19
* \|	Extraction: 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-04
\|\\|
\| *	Fix Haskell extraction for terms over 45 characters long	Nickolai Zeldovich	2016-05-04
\| *	Handle primitive projections inside types when extracting (bug #4616).	Guillaume Melquiond	2016-05-04
* \|	Merge branch 'haskell-type-indent' of https://github.com/zeldovich/coq into t...	Pierre Letouzey	2016-05-04
\|\ \
* \ \	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-04-24
\|\ \ \ \| \| \|/ \| \|/\|
* \| \|	Removing redundant *_TYPED AS clauses in EXTEND statements.	Pierre-Marie Pédrot	2016-04-12
\| * \|	Fix order of arguments to Big.compare_case in ExtrOcamlZBigInt.v	Nickolai Zeldovich	2016-04-09
* \| \|	Removing the special status of generic entries defined by Coq itself.	Pierre-Marie Pédrot	2016-03-17
\| \| *	Fix Haskell extraction for terms over 45 characters long	Nickolai Zeldovich	2016-02-19
\| \|/ \|/\|
* \|	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
* \|	merge	Matej Kosik	2016-01-11
\|\ \
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-06
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Protect code against changes in Map interface.	Maxime Dénès	2016-01-06
* \| \|	Merge remote-tracking branch 'origin/v8.5' into trunk	Guillaume Melquiond	2016-01-05
\|\\| \|
\| * \|	Extraction: msg_notice instead of msg_info.	Pierre Courtieu	2016-01-04
* \| \|	Merge branch 'v8.5' into trunk	Guillaume Melquiond	2015-12-31
\|\\| \|
* \| \|	Do not compose "str" and "to_string" whenever possible.	Guillaume Melquiond	2015-12-22
\| \|/ \|/\|
\| *	Inclusion of functors with restricted signature is now forbidden (fix #3746)	Pierre Letouzey	2015-12-22
\|/
*	Extraction: slightly better heuristic for Obj.magic simplifications	Pierre Letouzey	2015-12-16