coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[configure] fix detection of `md5sum`	Vincent Laporte	2017-12-04
\|
*	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 ↵	Maxime Dénès	2017-12-01
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	functionalization.
* \ \ \ \	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
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	#3125)
* \| \| \| \| \| \|	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 ↵	Maxime Dénès	2017-11-30
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	instance.
\| \| \| \| \| * \| \| \|	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
\| \|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
\| \| \| \| * \| \| \|	[lib] [api] Introduce record for `object_prefix`	Emilio Jesus Gallego Arias	2017-11-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is a minor cleanup adding a record in a try to structure the state living in `Lib`.
\| \| \| \| \| * \| \|	[proof] [api] Rename proof types in preparation for functionalization.	Emilio Jesus Gallego Arias	2017-11-29
\| \|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular `Proof_global.t` will become a first class object for the upper parts of the system in a next commit.
* \| \| \| \| \| \|	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 ↵	Maxime Dénès	2017-11-29
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of levels
* \ \ \ \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular singleton inductive types are considered injectable, even in the absence of the option "Set Keep Proof Equalities". This fixes #3125 (and #4560, #6273).
\| \| \| \| \| \| * \| \| \|	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This function returns InProp or InSet for inductive types only when the inductive type has been explicitly truncated to Prop or (impredicative) Set. For instance, singleton inductive types and small (predicative) inductive types are not truncated and hence in Type.
\| \| \| \| \| \| * \| \| \|	Moving non-recursive function sort_family_of out of the retype block of ↵	Hugo Herbelin	2017-11-28
\| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	recursive functions.
\| \| \| \| \| \| \| * /	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
\| \|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We remove the progs target [examples] to save time, we still build the full library thou. I guess we can't do better for now unless we get some Travis subscription.
\| \| \| \| \| *	CI: use -byte-only in [warnings] jobs.	Gaëtan Gilbert	2017-11-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This avoids mixing native and byte compilation as the debug printers are always byte compiled and the tools have no .byte rule, only the OCAMLBEST rule.
\| \| \| \| \| *	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; ↵	Maxime Dénès	2017-11-28
\|\ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	updating Camlp4->Camlp5.
\| \| \| \| \| \| * \|	[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
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	In particular, we put all the context in the atts structure, and generalize the type of the parameters of a vernac. I hope this helps people working on "attributes", my motivation is indeed having a more robust interpretation.
* \| \| \| \| \| \|	Merge PR #6237: coq_makefile tests: build in easily removed temporary ↵	Maxime Dénès	2017-11-27
\|\ \ \ \ \ \ \ \| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \|	subdirectory.
* \| \| \| \| \| \|	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
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \