coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Decimal goodies : conversion to/from Coq strings	Pierre Letouzey	2018-02-20
*	Decimal: proofs that conversions from/to nat,N,Z are bijections	Pierre Letouzey	2018-02-20
*	Decimal: simple representation of base-10 numbers	Pierre Letouzey	2018-02-20
*	Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...	Maxime Dénès	2018-02-19
\|\
* \	Merge PR #6761: Remove unused argument in Record.declare_structure	Maxime Dénès	2018-02-19
\|\ \
* \ \	Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`	Maxime Dénès	2018-02-19
\|\ \ \
* \ \ \	Merge PR #6753: [toplevel] Make toplevel state into a record.	Maxime Dénès	2018-02-19
\|\ \ \ \
* \ \ \ \	Merge PR #6230: Better Cemitcodes API + compact relocation representation	Maxime Dénès	2018-02-19
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6772: Cleanup inferCumulativity	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6648: [tactics] make apply_type safe	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6478: [build] Fix VM dynamic linking prep in byte builds.	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6571: Fix ci-all target	Maxime Dénès	2018-02-19
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| * \| \| \| \| \| \| \| \|	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
\| \| \| \| \| * \| \| \| \| \| \| \|	apply_type: add option "typecheck" passed down to refine	Enrico Tassi	2018-02-16
\| \|_\|_\|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \| \| \| \| * \| \| \| \| \| \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| \|_\|_\|_\|/ / / / / / / \|/\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Adding a test for the construction that was broken in Coccinelle.	Pierre-Marie Pédrot	2018-02-16
\| \| \| \| \| \| \| \| \| \| *	Extrude monomorphic universe contexts from with Definition constraints.	Pierre-Marie Pédrot	2018-02-16
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \| \|	[toplevel] Make toplevel state into a record.	Emilio Jesus Gallego Arias	2018-02-15
\| \| \| \| \| \| \| * \| \|	[ide] Localize a IDE-specific flag.	Emilio Jesus Gallego Arias	2018-02-15
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #1073: new quick2vo target: like vio2vo, but smarter	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	disable tests: vio2vo is broken in Windows	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \|	also test vio2vo	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \|	test "make quick2vo"	Ralf Jung	2018-02-15
\| * \| \| \| \| \| \| \| \|	new quick2vo target: like vio2vo, but smarter	Ralf Jung	2018-02-15
\| \| \|_\|_\|/ / / / / \| \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	coq_makefile: Support "" as the prefix in _CoqProject	Joachim Breitner	2018-02-15
* \| \| \| \| \| \| \| \| \|	Merge PR #6760: CHANGES for 8.7.2.	Maxime Dénès	2018-02-15
\|\ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \|	CHANGES for 8.7.2.	Théo Zimmermann	2018-02-14
\|/ / / / / / / / / /
\| \| \| \| \| \| \| \| \| *	Remove unused argument in Record.declare_structure	Gaëtan Gilbert	2018-02-14
\| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| * \|	Factorize the relocations in the on-disk VM representation.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| * \|	Use a more compact representation for bytecode relocations stored on disk.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| * \|	Do not use global variables for VM bytecode compilation in Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| * \|	Remove the unsafe bytes conversion function in Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| * \|	Move the call to the computation of bytecode inside Cemitcodes.	Pierre-Marie Pédrot	2018-02-14
\| \| \| \| \| \| \| * \|	Abstract further the type of VM bytecode compilation.	Pierre-Marie Pédrot	2018-02-14
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	detype_case predicate is not optional	Gaëtan Gilbert	2018-02-14
* \| \| \| \| \| \| \|	Merge PR #6742: Add CHANGES entry for #1047 (universe instance on Type notation)	Maxime Dénès	2018-02-14
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6713: Fix #6677: Critical bug with VM and universes	Maxime Dénès	2018-02-14
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| * \| \| \|	[build] Fix VM dynamic linking prep in byte builds.	Emilio Jesus Gallego Arias	2018-02-14
\| \| \| \| \|_\|/ / / / \| \| \| \|/\| \| \| \| \|
\| \| \| \| \| \| * \| \|	coqdev.el: wait for 'compile to touch compilation-error-regexp-alist	Gaëtan Gilbert	2018-02-13
\| \| * \| \| \| \| \| \|	Add CHANGES entry for #1047	Tej Chajed	2018-02-13
\| \| \|/ / / / / /
\| \| \| \| \| * \| \|	coqdev.el: fix "compilate"-command typo	Gaëtan Gilbert	2018-02-13
\| \| \| \| \| * \| \|	coqdev.el: shell-quote-argument the directory for make -C	Gaëtan Gilbert	2018-02-13
\| \| \| \| \| * \| \|	coqdev.el: stop using when-let for emacs<25 compatibility.	Gaëtan Gilbert	2018-02-13
* \| \| \| \| \| \| \|	Merge PR #6693: [toplevel] Refactor command line argument handling.	Maxime Dénès	2018-02-13
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6702: [vernac] [minor] Move print effects to top-level caller.	Maxime Dénès	2018-02-13
\|\ \ \ \ \ \ \ \ \