coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin	2008-07-23
*	Oops... forgot some debug code.	msozeau	2008-07-23
*	Add test-suite file for bug# 1905 and minor fix in Program/Equality.	msozeau	2008-07-22
*	New tactics [conv] to test convertibility (actually, unification) of two	msozeau	2008-07-22
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Autour du parsing:	herbelin	2008-07-15
*	Tentative de relecture des scripts de Mult.v au regard des tactiques actuelles	herbelin	2008-07-15
*	- Improve [Context] vernacular to allow arbitrary binders, not just	msozeau	2008-07-07
*	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey	2008-07-04
*	Fixes in handling of implicit arguments:	msozeau	2008-07-04
*	Various bug fixes in type classes and subtac:	msozeau	2008-07-01
*	QMake : alternative equivalences with Qcanon thanks to earlier irreducibility...	letouzey	2008-06-30
*	QMake: Proofs that add_norm and other ..._norm functions produce irreducible ...	letouzey	2008-06-28
*	Enhanced discrimination nets implementation, which can now work with	msozeau	2008-06-27
*	Some work on BigQ :	letouzey	2008-06-25
*	Rename obligations_tactic to obligation_tactic and fix bugs #1893.	msozeau	2008-06-22
*	typo in a comment	letouzey	2008-06-20
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	Temporary fix for bug #1876, printing fails because of unresolved	msozeau	2008-06-13
*	Changing the definitions of pred and minus in the style of GG	werner	2008-06-12
*	Zpow_facts.Zmult_power: kills a useless hypothesis	letouzey	2008-06-11
*	- Amélioration nommage dans EqdepFacts suivant remarque de Arthur C.	herbelin	2008-06-10
*	- Correct handling of DependentMorphism error, using tclFAIL instead of	msozeau	2008-06-10
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Enhancements to coqdoc, better globalization of sections and modules.	msozeau	2008-06-06
*	avoid duplicated creation of WFacts instances	letouzey	2008-06-06
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
*	In abstract parts of theories/Numbers, plus/times becomes add/mul,	letouzey	2008-06-03
*	In abstract parts of theories/Numbers, plus/times becomes add/mul,	letouzey	2008-06-02
*	Petites corrections diverses :	herbelin	2008-06-02
*	newton iteration for sqrt31	thery	2008-06-02
*	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey	2008-06-01
*	BigQ: starting to create and use an interface QSig	letouzey	2008-06-01
*	Enhance the BigN and BigZ infrastructure:	letouzey	2008-06-01
*	Improve the dependent induction tactic to automatically find the	msozeau	2008-05-30
*	NBigN: proofs that BigN implements axioms of NAxiomsSig	letouzey	2008-05-29
*	- Modification de la déf de minus et pred conformément aux remarques de	herbelin	2008-05-28
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	Cyclic31: no more Admitted, but I've cheated: sqrt31 and sqrt312 are	letouzey	2008-05-28
*	CyclicAxioms: after discussion with Laurent, znz_WW and variants are	letouzey	2008-05-28
*	- Correction bug highlighting "Module" dans Coqide	herbelin	2008-05-28
*	Cyclic31: proofs for addmuldiv31, tail031 and head031. Only two Admitted left !	letouzey	2008-05-28
*	Cyclic31: proof of auxiliary function iter_int31 + (failed) attempt at provin...	letouzey	2008-05-27
*	Correction du problème de complexité de Print Assumptions :	aspiwack	2008-05-27
*	Cyclic31: migrate auxiliary lemmas to their legitimate files	letouzey	2008-05-27
*	Cyclic31 : proof of the spec of gcd31	letouzey	2008-05-27
*	Int31 : gcd31 was wrong	letouzey	2008-05-26