coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack	2014-09-04
*	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack	2014-09-04
*	Add test-suite file for Case derivation on primitive records.	Matthieu Sozeau	2014-09-04
*	Add test suite files for closed bugs.	Matthieu Sozeau	2014-09-04
*	Fix bug #3563, making syntactic matching of primitive projections	Matthieu Sozeau	2014-09-04
*	Putting back normalized goals when entering them.	Pierre-Marie Pédrot	2014-09-03
*	Yes another remaining clearing bug with 'apply in'.	Hugo Herbelin	2014-09-03
*	Fixing printing of unreachable local tactics.	Pierre-Marie Pédrot	2014-09-03
*	Test-suite for bug #2818.	Pierre-Marie Pédrot	2014-09-03
*	Fixing bug #2818.	Pierre-Marie Pédrot	2014-09-03
*	Useless hooks in Tacintern.	Pierre-Marie Pédrot	2014-09-03
*	Code simplification in Tacenv.	Pierre-Marie Pédrot	2014-09-03
*	Print error messages with more hidden information based on α-equivalence .	Arnaud Spiwack	2014-09-03
*	sed -i.toto -e 's/Objective Caml/\{\ocaml\}/g' doc/refman/RefMan-*.tex	Pierre Boutillier	2014-09-03
*	Improve RefMan section about Coq_makefile	Pierre Boutillier	2014-09-03
*	Update RefMan with respect to new loadpath management	Pierre Boutillier	2014-09-03
*	Cbn in refman	Pierre Boutillier	2014-09-03
*	Additional entry tactic_arg in Print Grammar tactic.	Pierre-Marie Pédrot	2014-09-03
*	Code factorization in Tacintern.	Pierre-Marie Pédrot	2014-09-03
*	Cleaning code in Pptactic.	Pierre-Marie Pédrot	2014-09-02
*	Adding a test-suite for second-order matching order and indexes.	Pierre-Marie Pédrot	2014-09-02
*	Fixing bug #3136.	Pierre-Marie Pédrot	2014-09-02
*	Another fix than 19a7a5789c to avoid descend_in_conjunction to use	Hugo Herbelin	2014-09-02
*	An apply test.	Hugo Herbelin	2014-09-02
*	Fixup introduction of coqworkmgr	Pierre Boutillier	2014-09-02
*	Removing [revert] tactic from the AST.	Pierre-Marie Pédrot	2014-09-02
*	stm: use xlabel insted of label in dot (debug) output	Enrico Tassi	2014-09-02
*	coqworkmgr	Enrico Tassi	2014-09-02
*	Fix Declaremods.end_library (Closes: #3536)	Enrico Tassi	2014-09-02
*	Removing the 'inductive' parameter from tacexpr AST.	Pierre-Marie Pédrot	2014-09-01
*	Moving the decompose tactic out of the AST.	Pierre-Marie Pédrot	2014-09-01
*	In evarconv, do first-order unification of LetIn's properly, ensuring we comp...	Matthieu Sozeau	2014-09-01
*	Coqide prints succesive hyps of the same type on 1 line	Pierre Boutillier	2014-09-01
*	Code cleaning in Tacintern.	Pierre-Marie Pédrot	2014-09-01
*	Getting rid of atomic tactics in Tacenv.	Pierre-Marie Pédrot	2014-08-31
*	Moving code of tactic interpretation from Tacenv to Vernacentries.	Pierre-Marie Pédrot	2014-08-31
*	Simplify even further the declaration of primitive projections,	Matthieu Sozeau	2014-08-30
*	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot	2014-08-29
*	Simplification of Genarg unpackers.	Pierre-Marie Pédrot	2014-08-29
*	Not using a "cut" in descend_in_conjunctions induced more success. We	Hugo Herbelin	2014-08-29
*	Fixing commit 50237af2.	Pierre-Marie Pédrot	2014-08-29
*	Add test-suite file. Compute the name for the record binder in the	Matthieu Sozeau	2014-08-29
*	Fix bug when defining primitive projections mixing defined and abstracts fields.	Matthieu Sozeau	2014-08-29
*	Fixing bug #3528.	Pierre-Marie Pédrot	2014-08-28
*	Simplification of the tclCHECKINTERRUPT tactic.	Pierre-Marie Pédrot	2014-08-28
*	Change the way primitive projections are declared to the kernel.	Matthieu Sozeau	2014-08-28
*	Fix bugs #3484 and #3546.	Matthieu Sozeau	2014-08-28
*	There are some occurs-check cases that can be handled by imitation (using pru...	Matthieu Sozeau	2014-08-28
*	Fixing an unnatural selection of subterms larger than expected in the	Hugo Herbelin	2014-08-28
*	Cleaning and documenting a bit the Proofview.Refine module.	Pierre-Marie Pédrot	2014-08-28