coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| * \| \| \| \| \| \| \| \| \|	Print something after the build completed if it wasn't a runner failure.	Théo Zimmermann	2018-07-04
\|/ / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This can then be leveraged by @coqbot to know which builds to restart.
\| * / / / / / / / /	[ci] Avoid annoying detached head warning.	Emilio Jesus Gallego Arias	2018-07-04
\|/ / / / / / / / /
\| \| \| \| * / / / /	Make bin/ in makefile, not configure.	Gaëtan Gilbert	2018-07-04
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Add a shell.nix that is not pinned to satisfy some developers' preference.	Théo Zimmermann	2018-07-03
\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Refactor default.nix to use optionals.	Théo Zimmermann	2018-07-03
\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \|	Fix timing tools on NixOS.	Théo Zimmermann	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[test suite] Test case for attributes	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Document attributes.	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	fix syntax of .mlg	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Describe attributes in the documentation.	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] use a record for the contents of the “deprecated” attribute	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] use plain strings as attribute names	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The concrete syntax is still restricted to identifiers.
\| \| \| \| \| \| \| *	[vernac] indentation	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] Generic syntax for flags/attributes	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] Generic parsing rules for attributes	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] Add a “deprecated” attribute	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	Allow “Let”-defined coercions	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] Concrete syntax for attributes	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] mk_atts: an atts record with default values	Vincent Laporte	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| *	[vernac] attribute_of_flags	Vincent Laporte	2018-07-03
\| \|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Elaborate a [atts] record out of a list of flags.
\| * \| \| \| \| \|	Add a test build of Nix package to GitLab CI.	Théo Zimmermann	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We pin default.nix again to make the CI build predictable. As in Windows builds, we need to override the default before_script. As in other test-suite jobs, we export logs as artifacts on failure.
\| * \| \| \| \| \|	Adapt default.nix to allow nix-build to run the test-suite.	Théo Zimmermann	2018-07-03
\|/ / / / / /
* \| \| \| \| \|	Merge PR #7978: [ci] [docker] Make sure we don't install optional packages ↵	Gaëtan Gilbert	2018-07-03
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	with apt.
\| \| \| * \| \| \|	Add overlay for equations.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Library: use ocaml typing to show that we find at most 2 files	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Library.register_loaded_library: remove unused variable	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This one is a bit weird. Unused since 4d95eb4e878f375a69f1b48d8833801bf555fdd0 (kept semantics, the m is the same one outside and inside the call)
\| \| \| * \| \| \|	Glob_ops.rename_glob_vars: fix typo	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Glob_ops.fix_kind_eq: fix typo	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Pputils: fix typo	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Evarutil.(e_)new_Type: remove unused env argument	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Remove unused function Evd.whd_sort_variable	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Remove unused output of Universes.normalize_univ_variables	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Remove unused env argument to fresh_sort_in_family	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(Universes and Evd)
\| \| \| * \| \| \|	Coq_omega: remove unused Goal.enters	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since fd7f056b155b2ebaafa3251a3c136117ebefc3e3.
\| \| \| * \| \| \|	Remove unused function Coq_omega.timing.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Taccoerce: remove various unused arguments.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Remove unused arguments to Ide_slave.concl_next_tac.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since 2285dae8af54043090ce5f8a59aa4162679714c6
\| \| \| * \| \| \|	Pptactic: remove unused arguments	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	checker Indtypes: remove unused arguments	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
\| \| \| * \| \| \|	Term_typing: remove unused argument to internal function.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The function is defined with a typo but called with the same env that is mistakenly not shadowed. An alternative to this commit would be to fix the typo.
\| \| \| * \| \| \|	Cooking.cook_constant: remove unused env argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since d95306323 (remove template polymorphic definitions).
\| \| \| * \| \| \|	Indtypes: remove unused is_unit.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7607: Simplify reification of predicate in bytecode and native ↵	Pierre-Marie Pédrot	2018-07-03
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	compilers
\| \| \| \| * \| \| \|	checker Modops strengthening: remove unused argument resolver	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Subtyping.check_constant: remove unused module path argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Inductive.extract_stack,filter_stack_domain: remove unused arguments	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Nativecode compile_mind, compile_mind_field: remove unused arguments	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Nativecode.pp_mllam internal pp_letrec: remove unused argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Util.Empty: implement using polymorphic record.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	coqdoc Index.find_string: remove unused argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393.