aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2009-03-07- per session coq command stackvgross
2009-03-06fixed groebner as a plugin + pattern matching Timeoutbarras
2009-03-06missing Requirebarras
2009-03-06oups (module Entiers remplace par Big_int)barras
2009-03-05ajout de la tactique groebner de Loic Pottierbarras
2009-03-04illegal tactic application was having Ltac interpreter loopbarras
2009-03-04doc et CHANGES pour la commande Timeoutbarras
2009-03-04removed unused state filebarras
2009-03-04Timeout message was not always displayedbarras
2009-03-04commande Timeout + compaction des traces de debug_tacticbarras
2009-03-04Backtrack sur la mémoïsation de nf_evar.aspiwack
2009-03-04Temporary hack to make coqide.byte work (backport r11948) (see #2062)glondu
2009-03-04fixes to typecheck with old lablgtk.vgross
2009-03-03Hack to fix compilation problems. will be removed on lablgtk upgrade.vgross
2009-03-02porting r11900 11905 and 11953 to trunkbarras
2009-03-02Heavy modifications on the widget and edition tab creation mechanism.vgross
2009-02-27=?utf-8?q?Tentative=20d'optimisation=20(en=20temps)=20sur=20[nf=5Fevar]=20et=...aspiwack
2009-02-27extraction: update of README+CHANGES, rm of BUGS+TODOletouzey
2009-02-27Makefile: avoid building an empty contrib.cmxaletouzey
2009-02-24Amélioration de coq_makefilenotin
2009-02-23Add support for dependent "destruct" over terms in dependent types.herbelin
2009-02-20CoqInterface.vo in CONTRIBVO (should fix a dependency issue)letouzey
2009-02-20On passe les last_mods (un des champs de Evd.evar_defs) de listaspiwack
2009-02-20On ne met plus rien dans les last_mods tant que conv_pbs est vide.aspiwack
2009-02-20coq-interface and coq-parser can be calls to coqtop with adequate code dynlinkletouzey
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2009-02-17maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...jnarboux
2009-02-17#rectypes was already automatically added when using 3.11herbelin
2009-02-17Made hack to have Drop and #use"include" working with ocaml 3.10 publicherbelin
2009-02-16report de r11926: install de coqchkbarras
2009-02-16Fix [apply_in] which short-circuited resolution of evars in a custommsozeau
2009-02-13Bug 2050, commit v8.2 11923-11924 ---> trunksoubiran
2009-02-11Backport of 11890 from branch v8.2 (compile tools with the bestherbelin
2009-02-11Gestion des espaces dans les noms + guess_coqlib sous Windowsnotin
2009-02-11Nouvelle icône pour Coqnotin
2009-02-11Fix d'un petit problème de chemin sous Windowsnotin
2009-02-11Fix de divers petits problèmes d'installationnotin
2009-02-11Fix d'un problème lors de l'appel à coqtop avec un chemin relatifnotin
2009-02-11Modification du style du manuel de référencenotin
2009-02-11Report des revisions #11826, #11828 et #11829 de v8.2 vers trunknotin
2009-02-11A few fixes for bug #2032 (backport r11857)glondu
2009-02-11Add -coqtoolsbyteflags and -custom to ./configure...glondu
2009-02-11Document how FIND_VCS_CLAUSE has to be usedlmamane
2009-02-11config/revision.ml, git: handle case when not at tip of a branchlmamane
2009-02-11clean: revision is now called config/revision.mllmamane
2009-02-11Convert all uses of FIND_VCS_CLAUSE to recommended stylelmamane
2009-02-10Cyclic31: proof of a forgotten admitletouzey
2009-02-10removed prehistoric filesbarras
2009-02-10man page of coqchkbarras
2009-02-10Correction bug coqdev Hermann lehener.soubiran
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-03 23:18:21 +0000