aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2009-02-09commited complexity test for exponential behavior of unificationbarras
2009-02-09memoized is_ground_envbarras
2009-02-06pushed evar reduction in kernelbarras
2009-02-06Fixed bug #2036 (wrong copy-paste in RIneq) [copy of 11887 in branch v8.2]herbelin
2009-02-06Fixing #2044 (bad printing of primitive notation at the head ofherbelin
2009-02-06From v8.2 to trunk:herbelin
2009-02-04Fix [subrelation] clauses that privileged the weakest. Better impl argsmsozeau
2009-02-04Report r11631 from 8.2 and handle non-dependent goals better inmsozeau
2009-02-04Fix d'un bug avec l'option gallinanotin
2009-02-03Do not reserve the keyword "Infer".puech
2009-02-03Allow to turn contrib/subtac into a (nat)dynlink'able pluginletouzey
2009-02-03Fix the installation of plugins (both initial and late ones)letouzey
2009-01-31Reorder coqmktop options and document -echoglondu
2009-01-30More portable way to pipe stderrglondu
2009-01-30Correction bug 2037.soubiran
2009-01-29Solves some warning and hides some not-bad ones in doc. It remains aherbelin
2009-01-28FSet(Weak)List : eq_dec becomes Defined (and gets better proof)letouzey
2009-01-27- Fixed various Overfull in documentation.herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 17:08:51 +0000