coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Fix bug #1935, reworking the reflexivity, symmetry... tactics to use	msozeau	2008-09-03
*	Correct handling of implicit arguments in [Equations] definitions,	msozeau	2008-09-03
*	Add support for recursive definitions to [Equations], deciding if a	msozeau	2008-09-02
*	Initial implementation of a new command to define (dependent) functions by	msozeau	2008-09-02
*	Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about	herbelin	2008-09-02
*	Renaming parser -> coq-parser	glondu	2008-08-18
*	micromega : bug fixes and optimisations	fbesson	2008-08-07
*	Correction de bugs:	herbelin	2008-08-05
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Oops... the trunk behaviour is different	glondu	2008-07-29
*	Update test-suite output	glondu	2008-07-29
*	Fix bashism in test-suite/check	glondu	2008-07-28
*	Correction d'une incohérence de typage des inductifs polymorphes: les	herbelin	2008-07-25
*	A better test for relations being setoids or not: do leibniz rewrite iff	msozeau	2008-07-25
*	Add test-suite file for bug# 1905 and minor fix in Program/Equality.	msozeau	2008-07-22
*	Correct implementation of discharging of implicit arguments and add new	msozeau	2008-07-22
*	Uniformisation du format des messages d'erreur (commencent par une	herbelin	2008-07-17
*	Correction d'un autre bug autour de la gestion des niveaux vides de	herbelin	2008-07-11
*	test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq	letouzey	2008-07-09
*	Fix implicit arguments in sections bug and check for resolution of evars when	msozeau	2008-07-07
*	Micromega: doc + test-suite update	fbesson	2008-07-07
*	Prise en compte de changments dans subtac	notin	2008-07-03
*	Improved robustness of micromega parser. Proof search of Micromega test-suite...	fbesson	2008-07-02
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Préférence donnée aux constantes qui ne sont pas des projections	herbelin	2008-06-29
*	Micromega : bugs fixes - renaming of tactics - documentation	fbesson	2008-06-25
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	Propagation des révisions 11144 et 11136 de la 8.2 vers le trunk	herbelin	2008-06-18
*	- 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
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Renommage id dans le test Nametab (suite ajout d'une constante de ce	herbelin	2008-06-05
*	Temporarily disabling automatic test for bug 1338.v	notin	2008-06-03
*	Improve the dependent induction tactic to automatically find the	msozeau	2008-05-30
*	fixed bug #1780: a lift was missing (match predicate)	barras	2008-05-29
*	- Correction bug highlighting "Module" dans Coqide	herbelin	2008-05-28
*	Résolution bug #1850 sur notations avec niveaux inconnus de	herbelin	2008-05-26
*	Strategy commands are now exported	barras	2008-05-22
*	Correction bugs ide undo et highlight (suite à typos)	herbelin	2008-05-21
*	Corrections d'erreurs rapportées par Frédéric Besson sur le précédent	herbelin	2008-05-20
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
*	Fixed coqide bug #1856 that was introduced in revision 10915.	herbelin	2008-05-20
*	Retrait d'un test commité par erreur en 10947	herbelin	2008-05-20
*	Intégration de micromega ("omicron" pour fourier et sa variante sur Z,	herbelin	2008-05-19
*	Various fixes:	msozeau	2008-05-15
*	Résolution des problèmes ambigus d'inférence du type de retour des	herbelin	2008-05-14
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757	herbelin	2008-05-07
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05