coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| \| \| \| \| \| \| *	[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.
\| \| \| \| * \| \| \|	Coq_makefile.generate_conf_coq_config: remove unused argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Libobject.apply_dyn_fun: remove unused deflt argument	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since 8e07227c5853de78eaed4577eefe908fb84507c0.
\| \| \| \| * \| \| \|	CWarnings.normalize_flags: removed unused ~silent argument.	Gaëtan Gilbert	2018-07-03
\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \|	Modops.add_retroknowledge: remove unused argument.	Gaëtan Gilbert	2018-07-03
\| \|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Unused since fe1979bf47951352ce32a6709cb5138fd26f311d. I'm not sure if it was actually used back then since I didn't look at the function it was passed to.
* \| \| \| \| \| \|	Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands	Pierre-Marie Pédrot	2018-07-03
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7942: Extend readme with 'beginners guide'	Théo Zimmermann	2018-07-03
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7974: Fix default.nix following a package renaming.	Vincent Laporte	2018-07-03
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR #7977: allow `make check` to succeed when -prefix is given to ↵	Emilio Jesus Gallego Arias	2018-07-03
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	./configure and make install not run yet
\| \| \| \| \| \| * \| \| \| \|	[ci] [docker] Make sure we don't install optional packages with apt.	Emilio Jesus Gallego Arias	2018-07-02
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This should help towards ensuring that the system only has the packages we specify in the Dockerfile. We were missing: - `git`: used in the CI system itself! - `rsync`: used in the test-suite - `python3-setuptools`, `python3-wheel`: necessary to use pip3 properly to install the missing python package. - `autoconf`, `automake`: a few CI contribs depend on them.
* \| \| \| \| \| \| \| \| \| \|	Merge PR #7703: Add an option to force parameters to be uniform	Matthieu Sozeau	2018-07-02
\|\ \ \ \ \ \ \ \ \ \ \