coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Maxime Dénès	2018-03-08
\|\
* \	Merge PR #6744: Add String.concat	Maxime Dénès	2018-03-07
\|\ \
* \ \	Merge PR #6932: [stdlib] Do not use deprecated notations	Maxime Dénès	2018-03-07
\|\ \ \
* \ \ \	Merge PR #6905: Fix make ml-doc	Maxime Dénès	2018-03-07
\|\ \ \ \
* \ \ \ \	Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj`	Maxime Dénès	2018-03-07
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6922: Remove outdated information regarding the FAQ.	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6374: [toplevel] Modify printing goal strategy.	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #6790: Allow universe declarations for [with Definition].	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...)	Maxime Dénès	2018-03-07
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \|	[stdlib] Do not use deprecated notations	Vincent Laporte	2018-03-06
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \|	Remove outdated information regarding the FAQ.	Théo Zimmermann	2018-03-06
\| \|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The FAQ is not part of the Coq sources anymore.
* \| \| \| \| \| \| \|	Merge PR #6917: Fix failing packaging job.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of ↵	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	a record.
* \ \ \ \ \ \ \ \ \	Merge PR #6795: [ssreflect] Export parsing witnesses in mli file.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| *	ssr: use `apply_type ~typecheck:true` everywhere (fix #6634)	Enrico Tassi	2018-03-06
\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \|	Merge PR #6896: [compat] Remove NOOP deprecated options.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #6824: Remove deprecated options related to typeclasses.	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6900: [compat] Remove "Tactic Pattern Unification"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6901: [compat] Remove "Injection L2R Pattern Order"	Maxime Dénès	2018-03-06
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \| \| \|	[toplevel] Modify printing goal strategy.	Emilio Jesus Gallego Arias	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Instead of using a command-analysis heuristic, coqtop will now print goals if the goal has changed. We use a fast goal comparison heuristic, but a more refined strategy would be possible. This brings some [IMHO very welcome] change to PG and `-emacs`, which will now disable the printing of goals. Now, instead of playing with `Set/Unset Silent` and a bunch of other hacks, PG can issue a `Show` command whenever it wishes to redisplay the goals. This change will break PG, so we need to carefully coordinate this PR with PG upstream (see ProofGeneral/PG#212). Some interesting further things to do: - Detect changes in nested proofs. - Uncouple the silent flag from "print goals".
\| \| \| \| \| \| \| \| * \| \| \| \| \|	Fix failing packaging job.	Théo Zimmermann	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	gtksourceview depends transitively on py2cairo which was updated in Homebrew to depend explicitly on python2 (see Homebrew/homebrew-core#24714): this makes the python3 install step impossible. We also remove the libxml2 install step which was failing in a non-fatal way.
\| \| \| \| \| \| \| \| \| \| \| * \|	Remove NOPLUGINDOCS option	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Add empty description for @raise statements to satisfy ocamldoc	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Escape curly braces in ocamldoc comment	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Separate vim/emacs fold markers from ocamldoc comments	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	ocamldoc chokes on the markers {{{ and }}} because { and } are part of its syntax
\| \| \| \| \| \| \| \| \| \| \| * \|	Build docs for plugins by default, add NOPLUGINDOCS flag to disable	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Change non-documentation comment from ocamldoc style	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Fix formatting of some ocamldoc comments to reduce warnings	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Remove non-existent dependency	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Tweak comments to fix ocamldoc errors	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Tidy up ml-doc outut, give it a separate output directory	mrmr1993	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| * \|	Use computed deps to generate ml-doc and use implicit mli-doc deps	mrmr1993	2018-03-05
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \|	CHANGES and tests for with Definition @{univs}	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| * \| \|	Allow universe declarations for [with Definition].	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \|	[ssreflect] Export parsing witnesses in mli file.	Emilio Jesus Gallego Arias	2018-03-05
\| \|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is needed in order to manipulate/serialize SSR's AST. A quicker [and maybe better] alternative would be to just remove `ssrparser.mli`, as there are many grammar entries that still need exporting.
\| \| \| \| \| \| \| * \| \| \|	Sanitize universe declaration in Context (stop using a ref...)	Gaëtan Gilbert	2018-03-05
\| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When there is more than one variable to declare we stop trying to attach global universes (ie monomorphic or section polymorphic) to one of them.
* \| \| \| \| \| \| \| \| \|	Merge PR #6855: Update headers following #6543.	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad	Maxime Dénès	2018-03-05
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \|	[compat] Remove NOOP and alias deprecated options.	Emilio Jesus Gallego Arias	2018-03-04
\| \| \| \| \| \| \| \| \|/ / / \| \| \| \| \| \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Following up on #6791, we remove: - `Record Elimination Schemes`, a deprecated alias of `Nonrecursive Elimination Schemes` - `Match Strict` a deprecated NOOP.
\| \| \| \| \| \| * / \| \| \|	Remove deprecated options related to typeclasses.	Théo Zimmermann	2018-03-04
\| \| \| \| \| \| \|/ / / /
\| \| \| \| \| \| \| \| * \|	ssr: add Prenex Implicits for Some_inj to use it as a view	Anton Trunov	2018-03-04
\| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \|	ssr: fix typo in doc comment	Anton Trunov	2018-03-04
\| \| \| \| \| \| \| \|/ / \| \| \| \| \| \| \|/\| \|
* \| \| \| \| \| \| \| \|	Merge PR #935: Handling evars in the VM	Maxime Dénès	2018-03-04
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	ssr: ipats: V82.tactic ~nf_evars:false everywhere	Enrico Tassi	2018-03-04
\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	Proofview: V82.tactic option to not normalize evars	Enrico Tassi	2018-03-04
\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	ssr: rewrite Ssripats and Ssrview in the tactic monad	Enrico Tassi	2018-03-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed.
\| \| * \| \| \| \| \| \|	tactics: export e_reduct_in_concl	Enrico Tassi	2018-03-04
\| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \|	reductionops: remove dead code "bind_assum"	Enrico Tassi	2018-03-04
\| \| \| \| \| \| \| \| \|