coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \|	Merge PR #6912: [doc] Document removal of deprecated options.	Maxime Dénès	2018-03-15
\|\ \
* \ \	Merge PR #6967: [META] Update Coq version number.	Maxime Dénès	2018-03-15
\|\ \ \
\| \| \| *	[Sphinx] Add credits	Maxime Dénès	2018-03-15
\| \| \| *	[Sphinx] Move credits to new infrastructure	Maxime Dénès	2018-03-15
\| \|_\|/ \|/\| \|
* \| \|	Merge PR #6975: Fix whitespace issue in TacticNotationsVisitor.py	Maxime Dénès	2018-03-14
\|\ \ \
* \ \ \	Merge PR #6973: [Sphinx] migrate introduction	Maxime Dénès	2018-03-14
\|\ \ \ \
\| * \| \| \|	[Sphinx] Add introduction	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Move introduction to new infrastructure	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Add "edit on github"	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Mention license	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Remove ad-hoc color for links interfering with TOC	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Update some metadata	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Read version number from configure	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Comment out metadata for unused backends	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Remove information for .chm backend	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] add bibliography	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Add indexes	Maxime Dénès	2018-03-13
\| * \| \| \|	[Sphinx] Add table of contents	Maxime Dénès	2018-03-12
\| \| * \| \|	Fix whitespace issue in TacticNotationsVisitor.py	Maxime Dénès	2018-03-12
\| \|/ / / \|/\| \| \|
\| * \| \|	[Sphinx] Add doc preamble	Maxime Dénès	2018-03-12
\| * \| \|	[Sphinx] Add a few grammar constructions	Maxime Dénès	2018-03-12
\|/ / /
\| * /	[META] Update Coq version number.	Emilio Jesus Gallego Arias	2018-03-11
\|/ /
* \|	Merge PR #6869: [ssreflect] Fix module scoping problems due to packing and ml...	Maxime Dénès	2018-03-10
\|\ \
\| * \|	[ssreflect] Fix module scoping problems due to packing and mli files.	Emilio Jesus Gallego Arias	2018-03-10
\|/ /
* \|	Merge PR #6837: [located] Push inner locations in reference to a CAst.t node.	Maxime Dénès	2018-03-10
\|\ \
* \ \	Merge PR #6831: [located] More work towards using CAst.t	Maxime Dénès	2018-03-10
\|\ \ \
\| \| \| *	[doc] Document removal of deprecated options.	Emilio Jesus Gallego Arias	2018-03-09
\| \|_\|/ \|/\| \|
\| \| *	[located] Push inner locations in `reference` to a CAst.t node.	Emilio Jesus Gallego Arias	2018-03-09
\| \|/
\| *	[located] More work towards using CAst.t	Emilio Jesus Gallego Arias	2018-03-09
\|/
*	Merge PR #6946: Fix expected number of arguments for cumulative constructors.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6949: Revert PR #873: New strategy based on open scopes for decidin...	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Fix expected number of arguments for cumulative constructors.	Gaëtan Gilbert	2018-03-09
\| \|/ \|/\|
* \|	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09
* \| \|	Merge PR #6953: [default.nix] Pin nixpkgs version to include Sphinx dependencies	Maxime Dénès	2018-03-09
\|\ \ \
* \ \ \	Merge PR #6806: Adding missing unification constraint noticed by @skyskimmer	Maxime Dénès	2018-03-09
\|\ \ \ \
* \ \ \ \	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6923: Export options	Maxime Dénès	2018-03-09
\|\ \ \ \ \ \ \| \|_\|_\|_\|_\|/ \|/\| \| \| \| \|
\| \| \| \| * \|	[default.nix] Pin nixpkgs version to include Sphinx dependencies	Vincent Laporte	2018-03-09
\| \| \| \| * \|	[default.nix] minor cleaning	Vincent Laporte	2018-03-09
\| \|_\|_\|/ / \|/\| \| \| \|
\| \| \| \| *	Overlay for Elpi.	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Adjust EConstr.cmp_constructors for relaxed constructor cumulativity	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Documentation for Cumulativity Weak Constraints.	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Delayed weak constraints for cumulative inductive types.	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Statically enforce that ULub is only between levels.	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Option for messing with inference of irrelevant constraints	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| \| \| \| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
* \| \| \| \|	Merge PR #6480: Allow Prop as source for coercions	Maxime Dénès	2018-03-09
\|\ \ \ \ \ \| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #6947: coqide: queries from the query window are routed there (fix #...	Maxime Dénès	2018-03-09
\|\ \ \ \ \