coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Merge PR#201: Transparent abstract	Maxime Dénès	2017-05-11
\|\
* \	Merge PR#605: Report a useful error for dependent induction	Maxime Dénès	2017-05-05
\|\ \
* \ \	Merge PR#593: Functional choice <-> [inhabited] and [forall] commute	Maxime Dénès	2017-05-05
\|\ \ \
\| \| * \|	Report a useful error for dependent induction	Tej Chajed	2017-05-03
\| * \| \|	Functional choice <-> [inhabited] and [forall] commute	Gaetan Gilbert	2017-04-30
\| \|/ /
* / /	Add .dir-locals.el and _CoqProject files for emacs stdlib editing	Jason Gross	2017-04-28
\|/ /
* \|	Merge PR#584: Give andb_prop a simpler proof	Maxime Dénès	2017-04-27
\|\ \
* \| \|	Small typo in comment	Vadim Zaliva	2017-04-26
\| \| *	Add transparent_abstract tactic	Jason Gross	2017-04-25
\| \|/ \|/\|
\| *	Give andb_prop a simpler proof	Jason Gross	2017-04-25
\|/
*	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
\|\
* \	Merge PR#455: Farewell decl_mode	Maxime Dénès	2017-04-06
\|\ \
\| \| *	Merge branch 'origin/v8.5' into v8.6.	Hugo Herbelin	2017-04-06
\| \| \|\
* \| \| \	Merge PR#442: Allow interactive editing of Coq.Init.Logic	Maxime Dénès	2017-03-17
\|\ \ \ \
* \ \ \ \	Merge PR#451: Add η principles for sigma types	Maxime Dénès	2017-03-17
\|\ \ \ \ \
\| \| \| * \| \|	Farewell decl_mode	Enrico Tassi	2017-03-07
\| \|_\|/ / / \|/\| \| \| \|
* \| \| \| \|	A couple of other useful properties about compare_cont.	Hugo Herbelin	2017-03-03
* \| \| \| \|	Compatibility of iff wrt not and imp.	Hugo Herbelin	2017-03-03
\| * \| \| \|	Add η principles for sigma types	Jason Gross	2017-03-01
\| * \| \| \|	Remove some trailing whitespace in Init/Specif.v	Jason Gross	2017-03-01
\|/ / / /
\| \| \| *	Fixing a little bug in printing ex2 (type was printed "_" by default).	Hugo Herbelin	2017-02-23
\| * \| \|	Allow interactive editing of Coq.Init.Logic	Jason Gross	2017-02-21
\|/ / /
* / /	Ltac as a plugin.	Pierre-Marie Pédrot	2017-02-17
\|/ /
* \|	Remove v62 from stdlib.	Théo Zimmermann	2016-10-24
* \|	Replacing deprecated Implicit Arguments in prelude.	Maxime Dénès	2016-07-18
* \|	Remove the swap tactic from the prelude.	Maxime Dénès	2016-07-18
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
* \|	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-06-16
* \|	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
* \|	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-04-27
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \| \|	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
* \| \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
\| * \|	Remove Print Universe directive.	Matthieu Sozeau	2015-10-02
\| * \|	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
\| \| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\| \| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\| \|/ \|/\|
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Adding a notation { x & P } for { x : _ & P }.	Hugo Herbelin	2015-08-02
* \|	Tentatively setting cons and Some with 1st implicit argument maximal	Hugo Herbelin	2015-05-09
\|/
*	Fix various typos in documentation	Matěj Grabovský	2015-03-31
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond	2015-02-25
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin	2014-11-02