aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2009-01-27Cleaned CHANGES (rough backport of 11855 from v8.2 to trunk).herbelin
2009-01-27Forgot a file in r11859. Sorry...puech
2009-01-26Revert changes in pcoq functions to restore compatibility with contribspuech
2009-01-23Suppression de l'ancien logo (problèmes de droits)notin
2009-01-23Really compare evar maps in progress, due to merging in apply and othermsozeau
2009-01-23Petit nettoyage faisant suite au commit #11847 .aspiwack
2009-01-22Fix #2011 : an incorrect environment when extracting Module ... with ...letouzey
2009-01-22Util.split_at : for quadratic to linear complexityletouzey
2009-01-22Extraction Library works now when some files share the same short name (fix #...letouzey
2009-01-22Fixes in the documentation of [dependent induction] and test-suitemsozeau
2009-01-22configure: more adequate message explaining what -opt is doingletouzey
2009-01-22Fix d'un petit problème avec ocamlmklib en présence de l'option -camldirnotin
2009-01-22Remplacement de cp --parents par un script shnotin