coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Also a less intrusive Profile.init_profile.	Hugo Herbelin	2017-07-20
\| \| \| \| \| \|	Calling it only when there is something to profile, or when profiling is explicitly required with the profile flags, so that profiling in plugins is possible.
*	A less intrusive Profile.close_profile.	Hugo Herbelin	2017-07-20
\| \| \| \| \| \| \| \| \|	No need to call Gc functions nor Unix timing functions when there is nothing to report. Moreover, PMP observed problems with these functions in the debugger. PMP also reported that Gc.minor takes some noticeable time, so no need to trigger some when unneeded.
*	Merge PR #770: [proof] Move bullets to their own module.	Maxime Dénès	2017-07-19
\|\
* \	Merge PR #788: [API] Remove `open API` in ml files in favor of `-open API` flag.	Maxime Dénès	2017-07-19
\|\ \
* \ \	Merge PR #895: [ci] VST is now built with IGNORECOQVERSION=true.	Maxime Dénès	2017-07-19
\|\ \ \
\| * \| \|	[ci] VST is now built with IGNORECOQVERSION=true.	Théo Zimmermann	2017-07-18
\|/ / /
* \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It breaks ocamlmerlin.
\| \| \| \| * \|	[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 ↵	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	moved to Global).
* \ \ \ \ \ \	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 ↵	Maxime Dénès	2017-07-17
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	rather than colors
\| \| \| \| \| \| * \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch.
\| \| \| \| \| * \| \| \| \|	Removing a use of AUContext.instance in the STM.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We only delay monomorphic proofs in quick mode, so that their universe context will always be empty.
\| \| \| \| \| * \| \| \| \|	Removing the uses of abstraction-breaking code in Lemmas.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	I had to slightly tweak a test in order to work around a bug of simpl that loses universes constraints when refolding polymorphic fixpoints.
\| \| \| \| \| * \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This essentially means storing the abstract universe context in the typeclass data, and abstracting it when necessary.
\| \| \| \| \| * \| \| \| \|	Safer API for Global.body_of_constant and variants.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We aditionally return the abstract universe context inside the option. This is relatively painless as most uses were using the option as a boolean.
\| \| \| \| \| * \| \| \| \|	Safer API for Global.type_of_global_in_context.	Pierre-Marie Pédrot	2017-07-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We return the abstract context instead of an arbitrary instantiation.
\| \| \| \| \| * \| \| \| \|	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
\| \|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Adding a comment regarding De Bruijn universe indices in the kernel.	Pierre-Marie Pédrot	2017-07-12
\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	[travis] Display info on tested commit for PR builds.	Théo Zimmermann	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is made necessary by the fact that the displayed commit in the header of the build can be outdated if the build was restarted or took a long time to start. Sometimes, it is so old that the link to GitHub is a 404.
* \| \| \| \| \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The function turning a side-effect declaration into the corresponding entry was crazily wrong, as it used a named universe context quantifying over DeBruijn universe indices. Declaring such entries resulted in random anomalies. This fixes bug #5641.
\| \| * \| \| \| \| \| \|	Properly handling polymorphic inductive subtyping in the checker.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is the followup of the previous commit, this time implementing the correct algorithm in the checker.
\| \| * \| \| \| \| \| \|	Properly handling polymorphic inductive subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before this patch, inductive subtyping was enforcing syntactic equality of the variable instance, instead of reasoning up to alpha-renaming.
\| \| * \| \| \| \| \| \|	Cleaning up the implementation of module subtyping in the kernel.	Pierre-Marie Pédrot	2017-07-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We export a function in UGraph to check that a polymorphic instance is a subtype of another, instead of rolling up our own in module code. We also add a few tests for module subtyping in presence of polymorphic constants.