coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	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
\|
*	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
* \ \ \ \	Merge PR #7703: Add an option to force parameters to be uniform	Matthieu Sozeau	2018-07-02
\|\ \ \ \ \
\| \| \| \| \| *	Add Equations overlay	Matthieu Sozeau	2018-07-02
\| \| \| \| \| \|
* \| \| \| \| \|	Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions	Théo Zimmermann	2018-07-02
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7965: doc: Fix typesetting in Gallina extensions	Théo Zimmermann	2018-07-02
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	Clean up documentation around beginner's guide.	Siddharth Bhat	2018-07-02
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- move `README` to `README.md` to take advantage of markdown features - remove `setup.txt`, port the editor specific information to the wiki. Merge development information into `dev/doc/README.md`. Wiki merge link: https://github.com/coq/coq/wiki/DevelSetup. - Add new links to files into `dev/README.md`. - Remove stale `translate.txt`.
\| \| \| \| * \| \|	[envars] honor env variable COQLIB	Enrico Tassi	2018-07-02
\| \| \| \| \| \| \|
\| \| \| \| \| \| *	hints: add Hint Variables/Constants Opaque/Transparent commands	Matthieu Sozeau	2018-07-02
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* \| \| \| \| \|	Merge PR #7902: Use a homebrew parser to replace the GEXTEND extension ↵	Emilio Jesus Gallego Arias	2018-07-02
\|\ \ \ \ \ \ \| \|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|	points of Camlp5
* \| \| \| \| \|	Merge PR #7961: [api] Fix wrong deprecation warning (#7915)	Enrico Tassi	2018-07-02
\|\ \ \ \ \ \
\| \| \| \| \| \| *	Adding back ocp-index to default.nix.	Théo Zimmermann	2018-07-02
\| \| \| \| \| \| \|
\| \| \| \| \| \| *	Fix default.nix following a package renaming.	Théo Zimmermann	2018-07-02
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| \| *	Document option Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \|
\| \| \| \| \| *	Add test for Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \|
\| \| \| \| \| *	Add flag Uniform Inductive Parameters	Jasper Hugunin	2018-07-01
\| \| \| \| \| \|
\| \| \| \| \| *	Implement uniform parameters in ComInductive	Jasper Hugunin	2018-07-01
\| \|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Don't allow notations attached to uniform inductives
\| * \| \| \|	[api] Fix wrong deprecation warning (#7915)	Emilio Jesus Gallego Arias	2018-07-01
\|/ / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes: #7915. Due to a change in the original misctypes removal PR, the deprecation notice went out of sync.
* \| \| \|	Merge PR #7964: Document that GITURL variables shouldn't have a trailing ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	.git anymore.
* \ \ \ \	Merge PR #7410: Splitting primitive numeral parser/printer for positive, N, ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Z into three files
* \ \ \ \ \	Merge PR #7760: Fixes #7712 (an anomaly in reporting bad recursive notation ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	format).
* \ \ \ \ \ \	Merge PR #7759: Workaround to fix #7731 (printing not splitting line at ↵	Emilio Jesus Gallego Arias	2018-07-01
\|\ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	break hint).
\| \| \| \| \| \| \| *	doc: typesetting and hyperlinks in Syntax Extensions	Lysxia	2018-06-30
\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \|	Merge PR #7960: [build] Remove target binary before copy.	Enrico Tassi	2018-06-30
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7949: Split the Ssrmatching module between code and grammar rules.	Enrico Tassi	2018-06-30
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \|	Split the Ssrmatching module between code and grammar rules.	Pierre-Marie Pédrot	2018-06-30
\|/ / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fixes #7857.
\| \| \| \| \| \| * \|	Adding an overlay for the PR.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Documenting the transition strategy of GEXTEND.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_tactic to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_toplevel to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_vernac to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_proofs to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_constr to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Port g_prim to the homebrew GEXTEND parser.	Pierre-Marie Pédrot	2018-06-29
\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	Use a homebrew parser to replace the GEXTEND extension points of Camlp5.	Pierre-Marie Pédrot	2018-06-29
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The parser is stupid and the syntax is almost the same as the previous one. The only difference is that one needs to wrap OCaml code between { braces } so that quoting works out of the box. Files requiring such a syntax are handled specifically by the type system and need to have a .mlg extension instead of a .ml4 one.