aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Initial implementation of a new command to define (dependent) functions byGravatar msozeau2008-09-02
* - Remove some dead code in subtacGravatar msozeau2008-09-02
* fixed minor environment issues when checking inductive typesGravatar barras2008-09-02
* fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...Gravatar barras2008-09-02
* added Makefile target: validate (to recheck all .vo in a row)Gravatar barras2008-09-02
* avoid small overflowsGravatar barras2008-09-02
* [checker] basic conversion oracle: expand local vars firstGravatar barras2008-09-02
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* Fix implementation of "Global Instance" which redeclared the sameGravatar msozeau2008-08-27
* Major speed and space improvements in setoid rewrite:Gravatar msozeau2008-08-27
* Little cleanup in auto.Gravatar msozeau2008-08-27
* Give back progress information after feeding the Program Instance to theGravatar msozeau2008-08-26
* Fix dependency problem that makes compilation fail :)Gravatar msozeau2008-08-23
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Typo (corrige le bug #1928)Gravatar notin2008-08-22
* Fixes in dependent induction tactic to keep names, allow givingGravatar msozeau2008-08-21
* Various fixes w.r.t typeclasses and subtac: resolve tcs properly insideGravatar msozeau2008-08-21
* Revert commit 11326, to see if it is what makes bench failGravatar glondu2008-08-18
* Renaming parser -> coq-parserGravatar glondu2008-08-18
* Install csdpcert with librariesGravatar glondu2008-08-16
* Mind environment variables in (generated) coq_config.mlGravatar glondu2008-08-16
* Fix build/install failures when ocamlopt is not availableGravatar glondu2008-08-16
* Add coqide manpage (taken from Debian)Gravatar glondu2008-08-12
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-01 13:58:51 +0000