aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-09-02added Makefile target: validate (to recheck all .vo in a row)barras
2008-09-02avoid small overflowsbarras
2008-09-02[checker] basic conversion oracle: expand local vars firstbarras
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-08-27Fix implementation of "Global Instance" which redeclared the samemsozeau
2008-08-27Major speed and space improvements in setoid rewrite:msozeau
2008-08-27Little cleanup in auto.msozeau
2008-08-26Give back progress information after feeding the Program Instance to themsozeau
2008-08-23Fix dependency problem that makes compilation fail :)msozeau
2008-08-22- New auto hints for transparency/opacity control, not bound to msozeau
2008-08-22Typo (corrige le bug #1928)notin
2008-08-21Fixes in dependent induction tactic to keep names, allow givingmsozeau
2008-08-21Various fixes w.r.t typeclasses and subtac: resolve tcs properly insidemsozeau
2008-08-18Revert commit 11326, to see if it is what makes bench failglondu
2008-08-18Renaming parser -> coq-parserglondu
2008-08-16Install csdpcert with librariesglondu
2008-08-16Mind environment variables in (generated) coq_config.mlglondu
2008-08-16Fix build/install failures when ocamlopt is not availableglondu
2008-08-12Add coqide manpage (taken from Debian)glondu
2008-08-08Various fixes in manpagesglondu
2008-08-07Suite commit #11311notin
2008-08-07micromega : bug fixes and optimisationsfbesson
2008-08-07eviter redondance du message d'erreur (Error while reading / File)barras
2008-08-07coqc: warning de l'option -dump-glob (unused case)barras
2008-08-06Mise à jour des fichiers README et INSTALL de la doc (bug #1921) + suppressi...notin
2008-08-06Add lemmas on lists: nth_default_eq, map_nth_errorglondu
2008-08-06correction : coqart is already publishedjnarboux
2008-08-05Correction de bugs:herbelin
2008-08-05Correction bug de filtrage sous-terme #1920 introduit dans commitherbelin
2008-08-05Suite 11187 et 11298 : ne retarder le dépliage d'une projectionherbelin
2008-08-04Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parherbelin
2008-08-04Évolutions diverses et variées.herbelin
2008-07-31Corrige un bug du commit 11187 (le comportement à respecter étaitherbelin
2008-07-29Oops... the trunk behaviour is differentglondu
2008-07-29Update test-suite outputglondu
2008-07-29Typo in docglondu
2008-07-29Backport r11289.msozeau
2008-07-28Fix typoglondu
2008-07-28Use COQINSTALLPREFIX for doc tooglondu
2008-07-28Fix bashism in test-suite/checkglondu
2008-07-28Remove pcoq from check prerequisitesglondu
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
2008-07-28Fix wrong environment bug in test for setoid_rewrite or rewrite.msozeau
2008-07-28Fix bug in term dnet preventing some unifications. Allow "higher-order"msozeau
2008-07-28Show configure choice for browser in CoqIDE preferencesglondu
2008-07-27Now, -browser option is effective (and compiles)glondu
2008-07-27(Partially) Revert previous commit because of FTBFSglondu
2008-07-27Add -browser option to configure scriptglondu
2008-07-27Oups (on refait le 11268 en mieux)herbelin
2008-07-26Even better test for choosing rewrite or setoid_rewrite.msozeau