coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \|	Merge PR #781: Remove dead code [Universes.simplify_universe_context]	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #783: Remove some useless code in Term_typing	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #822: [meta] [api] Fix META file for API introduction.	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \|	[funind] Remove spurious character in comment.	Emilio Jesus Gallego Arias	2017-07-17
\| \| \| \| * \| \| \| \| \| \| \| \|	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
\| \| \| \| * \| \| \| \| \| \| \| \|	[meta] [api] Fix META file for API introduction.	Emilio Jesus Gallego Arias	2017-07-17
\| \|_\|_\|/ / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #878: Prepare De Bruijn universe abstractions, Episode II: Upper layers	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #881: Adapting base_include to 91df40272 (body_of_constant_body move...	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #879: Adding debug printers related to universes	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #874: Adding econstr printer to "include" file.	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #872: [travis] Display info on tested commit for PR builds.	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #865: RefMan-ext: fix some typos	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #862: Adding support for bindings tags to explicit prefix/suffix rat...	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| * \ \ \ \ \ \	Merge PR #861: Fix typo in documentation for identity	Maxime Dénès	2017-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \|\ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Adapting to 91df40272 (body_of_constant_body moved to global).	Hugo Herbelin	2017-07-16
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update with non structurally recursive	william-lawvere	2017-07-14
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding debug printers related to universes in the default debugger source file.	Pierre-Marie Pédrot	2017-07-14
\| \|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Fix a typo in dev/changes.	Pierre-Marie Pédrot	2017-07-14
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Document the changes in API brought by this series of patches.	Pierre-Marie Pédrot	2017-07-14
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Getting rid of abstraction breaking code in tclABSTRACT.	Pierre-Marie Pédrot	2017-07-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[travis] Update testing to 4.05.0 + Camlp5 7.01	Emilio Jesus Gallego Arias	2017-07-13
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Removing a use of AUContext.instance in the STM.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Removing the uses of abstraction-breaking code in Lemmas.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| * \| \| \| \| \| \|	Set version to 8.7+alpha.	Maxime Dénès	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Removing the uses of abstraction-breaking code in Obligations.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Remove the function Global.type_of_global_unsafe.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	The only abstraction-breaking function in Univ is now AUContext.instance.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Getting rid of AUContext abstraction breakers in Elimschemes.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Getting rid of AUContext abstraction breakers in Discharge.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Make the typeclass implementation fully compatible with universe polymorphism.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Safer API for Global.type_of_global_in_context.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Getting rid of AUContext abstraction breakers in Record.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Getting rid of AUContext abstraction breakers in Search.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Getting rid of AUContext abstraction breakers in Recordops.	Pierre-Marie Pédrot	2017-07-13
\| \|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #870: Prepare De Bruijn universe abstractions, Episode I: Kernel	Maxime Dénès	2017-07-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	Adding econstr printer to "include" file.	Hugo Herbelin	2017-07-12
\| \|_\|_\|_\|/ / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	format pairs of items for pr_depth to get alternating separators	Paul Steckler	2017-07-12
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Adding a comment regarding De Bruijn universe indices in the kernel.	Pierre-Marie Pédrot	2017-07-12
\| \| \| \| \| \| \| \| \| \| \| \| \| \| * \|	Remove deprecated options from ./configure	Théo Zimmermann	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	Sync the manual with the deprecation warnings.	Théo Zimmermann	2017-07-11
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \|	[travis] Display info on tested commit for PR builds.	Théo Zimmermann	2017-07-11
\| \| \| \| \| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Backtracking on deprecation of Bracketing Last Intro Pattern.	Théo Zimmermann	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Deprecate options that were introduced for compatibility with 8.5.	Théo Zimmermann	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \|/ / \| \| \| \| \| \| \| \| \| \| \| \|/\| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #871: Update Travis badge following the switch to master	Maxime Dénès	2017-07-11
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Update Travis badge following the switch to master	Théo Zimmermann	2017-07-11
\| \| \|_\|_\|/ / / / / / / / / / \| \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Moving the last bits of abtraction-breaking code out of the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Fix nonsensical universe abstraction in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Properly handling polymorphic inductive subtyping in the checker.	Pierre-Marie Pédrot	2017-07-11