coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove redundant Zcase from the checker.	Pierre-Marie Pédrot	2017-12-02
*	Merge PR #736: [ci] Test coqchk on the CompCert target.	Maxime Dénès	2017-12-01
\|\
* \	Merge PR #6256: CI: better ocaml warning checks	Maxime Dénès	2017-12-01
\|\ \
* \ \	Merge PR #6276: Coqchk accepts filenames	Maxime Dénès	2017-12-01
\|\ \ \
* \ \ \	Merge PR #6233: [proof] [api] Rename proof types in preparation for functiona...	Maxime Dénès	2017-12-01
\|\ \ \ \
* \ \ \ \	Merge PR #1049: Remove obsolete locality	Maxime Dénès	2017-11-30
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6244: [lib] [api] Introduce record for `object_prefix`	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \
\| \| \| \| \| \| *	[ci] Test coqchk on the CompCert target.	Théo Zimmermann	2017-11-30
* \| \| \| \| \| \|	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6269: [ci] [vst] Shorten compilation time to avoid Travis timeouts.	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6193: Fix (partial) #4878: option to stop autodeclaring axiom as in...	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \
\| \| \| \| \| * \| \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \| \| * \| \|	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6271: Add PR backport script.	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6253: Fixing inconsistent associativity of level 10 in the table of...	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6199: [vernac] Uniformize type of vernac interpretation.	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \|	coq_makefile: pass filenames to coqchk	Ralf Jung	2017-11-29
\| \| \| \| \| \| \| \| * \|	Documenting the possibility to pass filenames to coqchk.	Pierre-Marie Pédrot	2017-11-29
\| \| \| \| \| \| \| \| * \|	Allow to pass physical files to coqchk.	Pierre-Marie Pédrot	2017-11-29
\| \| \| \| \| \| * \| \| \|	In injection/inversion, consider all template-polymorphic types as injectable.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| * \| \| \|	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| * \| \| \|	Moving non-recursive function sort_family_of out of the retype block of recur...	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \|/ / /
\| \| \| \| \| \| \| * /	Adding an interface file for checker/check.ml.	Pierre-Marie Pédrot	2017-11-28
\| \|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \|
\| \| \| * \| \| \| \|	Add PR backport script.	Théo Zimmermann	2017-11-28
\| \|_\|/ / / / / \|/\| \| \| \| \| \|
\| \| \| \| * \| \|	[ci] [vst] Shorten compilation time to avoid Travis timeouts.	Emilio Jesus Gallego Arias	2017-11-28
\| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| \| \| \| *	CI: use -byte-only in [warnings] jobs.	Gaëtan Gilbert	2017-11-28
\| \| \| \| \| *	Fix native compute for byte compiled Coq.	Gaëtan Gilbert	2017-11-28
\| \| \| * \| \|	Fix (partial) #4878: option to stop autodeclaring axiom as instance.	Gaëtan Gilbert	2017-11-28
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| \| *	Travis: do not build stdlib in [warnings] jobs.	Gaëtan Gilbert	2017-11-28
\| \|_\|_\|/ \|/\| \| \|
* \| \| \|	Merge PR #6259: Add PR merge script.	Maxime Dénès	2017-11-28
\|\ \ \ \
\| * \| \| \|	Add PR merge script.	Maxime Dénès	2017-11-28
* \| \| \| \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6235: Fixing failing mkdir in test-suite for coq-makefile.	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6248: [api] Remove aliases of `Evar.t`	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6246: Ref. Man.: Updating the current official writing of OCaml; up...	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	[vernac] Adjust `interp` to pass polymorphic in the attributes.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| \| \| \| * \|	[vernac] Add polymorphic to the type of vernac interpration options.	Emilio Jesus Gallego Arias	2017-11-27
\| \| \| \| \| \| * \|	[vernac] Start to uniformize type of vernac interpretation.	Emilio Jesus Gallego Arias	2017-11-27
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6237: coq_makefile tests: build in easily removed temporary subdire...	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #6242: Use Evarutil.has_undefined_evars for tactic has_evar.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6236: Fix coq-makefile ocamldoc call when configured with -annotate.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6207: [stm] Allow delayed constant in interactive mode.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #6238: Fix deprecated syntax warning from vernacextend.mlp.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6241: [lib] Generalize Control.timeout type.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6228: Make byte on gitlab.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6226: Enhance votour	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6149: Update TimeFileMaker.py to correctly sort timing diffs	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6041: Protecting the printing of filenames with space	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6227: Linter: do not lint untracked files.	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \