coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #783: Remove some useless code in Term_typing	Maxime Dénès	2017-07-17
\|\
* \|	Fix nonsensical universe abstraction in the kernel.	Pierre-Marie Pédrot	2017-07-11
* \|	Getting rid of simple calls to AUContext.instance.	Pierre-Marie Pédrot	2017-07-11
* \|	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
* \|	Clean up universes of constants and inductives	Amin Timany	2017-06-16
* \|	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
\| *	Remove some useless code in Term_typing	Gaëtan Gilbert	2017-06-13
* \|	[kernel] Improve proof using message, fixes bugzilla #3613	Emilio Jesus Gallego Arias	2017-06-07
\|/
*	Merge PR#441: Port Toplevel to the Stm API	Maxime Dénès	2017-04-12
\|\
\| *	[stm] Remove edit_id.	Emilio Jesus Gallego Arias	2017-04-12
* \|	Merge PR#537: Efficient side-effect abstraction	Maxime Dénès	2017-04-11
\|\ \ \| \|/ \|/\|
* \|	Inline the only use of hcons_j in Term_typing.	Pierre-Marie Pédrot	2017-04-07
* \|	Documenting the fact terms are only hashconsed outside of a section.	Pierre-Marie Pédrot	2017-04-06
\| *	Fix substitution of abstracted lemmas.	Pierre-Marie Pédrot	2017-04-04
* \|	More efficient check in validity of side-effects.	Pierre-Marie Pédrot	2017-03-27
* \|	Fix hashconsing of terms in the kernel.	Pierre-Marie Pédrot	2017-03-27
\|/
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-24
\|\
\| *	Using a dedicated datastructure for side effect ordering.	Pierre-Marie Pédrot	2017-03-23
\| *	Making the side_effects type opaque.	Pierre-Marie Pédrot	2017-03-23
* \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\\|
\| *	Add a few comments in term_typing.ml.	Maxime Dénès	2017-03-21
\| *	Do not typecheck twice the type of opaque constants.	Maxime Dénès	2017-03-21
* \|	Merge PR#134: Enable `-safe-string`	Maxime Dénès	2017-03-21
\|\ \
\| * \|	[safe_string] kernel/term_typing	Emilio Jesus Gallego Arias	2017-03-14
* \| \|	[future] Remove unused parameter greedy.	Emilio Jesus Gallego Arias	2017-03-14
\|/ /
* \|	Replace Typeops by Fast_typeops	Gaetan Gilbert	2016-12-12
* \|	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\ \
* \| \|	CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...	Matej Kosik	2016-08-30
* \| \|	CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...	Matej Kosik	2016-08-25
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \|/ \|/\|
\| *	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
\|/
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	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
*	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
* \|	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-03-05
\|\ \
\| * \|	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-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
* \| \|	merge	Matej Kosik	2016-01-11
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \| \|	Fix handling of side-effects in case of `Opaque side-effects as well.	Matthieu Sozeau	2016-01-04
* \| \|	Fix bug #4456, anomaly in handle-side effects	Matthieu Sozeau	2015-12-31
\|/ /
* \|	Cleanup API and comments of 908dcd613	Enrico Tassi	2015-10-29
* \|	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28