coq - The formal proof system

Age	Commit message (Expand)	Author
2020-12-11	Merge PR #13519: Better primitive type support in custom string and numeral n...	coqbot-app[bot]
2020-12-11	Merge PR #13540: Clean support of primitive integers	Pierre-Marie Pédrot
2020-12-09	Please the god of nitpicking by renaming the shift monoid operations.	Pierre-Marie Pédrot
2020-12-09	Document Esubst API and implementation.	Pierre-Marie Pédrot
2020-12-09	Compact representation of identity substitutions.	Pierre-Marie Pédrot
2020-12-09	Optimization: take advantage that we don't use arrays anymore in substitutions.	Pierre-Marie Pédrot
2020-12-09	More efficient implementation for substitutions.	Pierre-Marie Pédrot
2020-12-09	Cleanup substitution API.	Pierre-Marie Pédrot
2020-12-04	Better primitive type support in custom string and numeral notations.	Fabian Kunze
2020-12-02	Move *_with_full_binders variants out of the kernel.	Pierre-Marie Pédrot
2020-12-02	Make sure the msb is clear.	Guillaume Melquiond
2020-12-02	Greatly simplify the conversion functions between Z.t and Uint63.t.	Guillaume Melquiond
2020-12-01	Make the code clearer and faster by calling mask63 explicitly at the end.	Guillaume Melquiond
2020-12-01	Avoid compiler warnings.	Guillaume Melquiond
2020-12-01	Added comment about l2r in check_correct_arity	Gaëtan Gilbert
2020-12-01	Use ~l2r:true to restore previous order of unfolding when typing predicates o...	Matthieu Sozeau
2020-11-30	Merge PR #13501: [kernel] Fix #13495: incompleteness in cases typing for cumu...	coqbot-app[bot]
2020-11-27	[kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ...	Matthieu Sozeau
2020-11-26	[environ] [typing_flags] Introduce helper function to remove duplicate code	Emilio Jesus Gallego Arias
2020-11-26	[kernel] Allow to set typing flags in add_mind [inductive]	Emilio Jesus Gallego Arias
2020-11-26	[kernel] Allow to set typing flags in add_constant	Emilio Jesus Gallego Arias
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-24	Merge PR #13411: Rename the confusing neutral annotation in CClosure.	coqbot-app[bot]
2020-11-21	Rename the confusing neutral annotation in CClosure.	Pierre-Marie Pédrot
2020-11-20	Make sure accumulators do not exceed the minor heap (partly fix #11170).	Guillaume Melquiond
2020-11-19	Merge PR #12959: Improve the bytecode interpreter	Pierre-Marie Pédrot
2020-11-17	Merge PR #13397: Adding heterogeneous map on named contexts.	Pierre-Marie Pédrot
2020-11-16	Adding heterogeneous map on named contexts.	Hugo Herbelin
2020-11-16	Improve bad variance error message: mention expected and actual variances	Gaëtan Gilbert
2020-11-16	Syntax for specifying cumulative inductives	Gaëtan Gilbert
2020-11-16	Infrastructure for cumulative inductive syntax (no grammar extension yet)	Gaëtan Gilbert
2020-11-15	Merge PR #13356: Make the universe of primitive arrays irrelevant	Pierre-Marie Pédrot
2020-11-13	Merge PR #13358: Merge the Linked / LinkedInteractive native link information...	coqbot-app[bot]
2020-11-13	Hardcode next_up and next_down instead of relying on nextafter.	Guillaume Melquiond
2020-11-13	Add allocation-free variants of the nextup and nextdown floating-point operat...	Guillaume Melquiond
2020-11-13	Remove floating-point comparison operators as they are no longer needed.	Guillaume Melquiond
2020-11-13	Turn coq_float64.h into a .c file as it is no longer needed by coq_interp.c.	Guillaume Melquiond
2020-11-13	Inline the functions from coq_float64.h.	Guillaume Melquiond
2020-11-13	Make callback opcodes more generic.	Guillaume Melquiond
2020-11-13	Optimize Is_accu a bit.	Guillaume Melquiond
2020-11-13	Improve documentation of closure representations.	Guillaume Melquiond
2020-11-13	Turn Ksequence into a unary opcode, as its binary structure was never used.	Guillaume Melquiond
2020-11-13	Remove unused if-then-else construct from VM.	Guillaume Melquiond
2020-11-13	Restore discard_dead_code and use it to simplify match-with constructs.	Guillaume Melquiond
2020-11-13	Remove some unused opcodes from VM.	Guillaume Melquiond
2020-11-13	Remove unchecked arithmetic operations from VM, as they are not used.	Guillaume Melquiond
2020-11-13	Optimize handling of the VM stack with respect to the GC.	Guillaume Melquiond
2020-11-13	Make the universe of primitive arrays irrelevant	Gaëtan Gilbert
2020-11-13	Remove unused CClosure.FNativeEntries.farray	Gaëtan Gilbert
2020-11-12	Merge PR #13351: Fixes #13349: accept Search on subparts of an identifier, no...	coqbot-app[bot]