aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Various fixes in manpagesGravatar glondu2008-08-08
* Suite commit #11311Gravatar notin2008-08-07
* micromega : bug fixes and optimisationsGravatar fbesson2008-08-07
* eviter redondance du message d'erreur (Error while reading / File)Gravatar barras2008-08-07
* coqc: warning de l'option -dump-glob (unused case)Gravatar barras2008-08-07
* Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...Gravatar notin2008-08-06
* Add lemmas on lists: nth_default_eq, map_nth_errorGravatar glondu2008-08-06
* correction : coqart is already publishedGravatar jnarboux2008-08-06
* Correction de bugs:Gravatar herbelin2008-08-05
* Correction bug de filtrage sous-terme #1920 introduit dans commitGravatar herbelin2008-08-05
* Suite 11187 et 11298 : ne retarder le dépliage d'une projectionGravatar herbelin2008-08-05
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Corrige un bug du commit 11187 (le comportement à respecter étaitGravatar herbelin2008-07-31
* Oops... the trunk behaviour is differentGravatar glondu2008-07-29
* Update test-suite outputGravatar glondu2008-07-29
* Typo in docGravatar glondu2008-07-29
* Backport r11289.Gravatar msozeau2008-07-29
* Fix typoGravatar glondu2008-07-28
* Use COQINSTALLPREFIX for doc tooGravatar glondu2008-07-28
* Fix bashism in test-suite/checkGravatar glondu2008-07-28
* Remove pcoq from check prerequisitesGravatar glondu2008-07-28
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* Fix wrong environment bug in test for setoid_rewrite or rewrite.Gravatar msozeau2008-07-28
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Show configure choice for browser in CoqIDE preferencesGravatar glondu2008-07-28
* Now, -browser option is effective (and compiles)Gravatar glondu2008-07-27
* (Partially) Revert previous commit because of FTBFSGravatar glondu2008-07-27
* Add -browser option to configure scriptGravatar glondu2008-07-27
* Oups (on refait le 11268 en mieux)Gravatar herbelin2008-07-27
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
* Suite 11266 (warning tools/gallina.ml)Gravatar herbelin2008-07-25
* Correction d'une incohérence de typage des inductifs polymorphes: lesGravatar herbelin2008-07-25
* Fixed bug #1904 (instances of evars were no longer substituted sinceGravatar herbelin2008-07-25
* A better test for relations being setoids or not: do leibniz rewrite iffGravatar msozeau2008-07-25
* More compatibility fixes, revert the tauto fix that preventedGravatar msozeau2008-07-25
* Tauto breaking not only binary "conjunctions" seems like a bad ideaGravatar msozeau2008-07-24
* A (safe) implementation of prolog's cut in the typeclasses eauto to avoidGravatar msozeau2008-07-24
* Fix bug #1913, checking for unresolved evars which aren't obligations.Gravatar msozeau2008-07-24
* fixed loop in dependency fold of the checkerGravatar barras2008-07-24
* moved magic numbers to configure (share coq/coqchk)Gravatar barras2008-07-24
* broke cyclic dependenciesGravatar barras2008-07-24
* Suite commit 11236Gravatar notin2008-07-24
* Propagation de l'information "strict" (càd à toplevel ou en train deGravatar herbelin2008-07-24
* Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized theGravatar herbelin2008-07-23
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* Oops... forgot some debug code.Gravatar msozeau2008-07-23
* Add test-suite file for bug# 1905 and minor fix in Program/Equality.Gravatar msozeau2008-07-22
* New tactics [conv] to test convertibility (actually, unification) of twoGravatar msozeau2008-07-22