| Commit message (Expand) | Author | Age |
* | Coqdoc: also try coqlib relative to the coqdoc binary location | letouzey | 2011-04-20 |
* | Add directories in COQPATH to search path. | herbelin | 2011-04-14 |
* | Reorder search path order, so the standard library is search last. | herbelin | 2011-04-14 |
* | Applying Tom Prince's patch to coqdep not correctly applying the -R visibility | herbelin | 2011-04-08 |
* | A kind of reply to bug 2444 | pboutill | 2011-04-08 |
* | Fix last commit about coqdep: not everyone has a user-contrib dir | letouzey | 2011-04-03 |
* | Adjust coqdep so that it behaves like coqtop with respect to the user-contrib... | gmelquio | 2011-04-01 |
* | Remove the "Boxed" syntaxes and the const_entry_boxed field | letouzey | 2011-01-28 |
* | Fixed status of ÷ and × in coqdoc (they were seen as letter instead of symb... | herbelin | 2010-12-06 |
* | Better fix to bug #2183 ("moduleid" internal name got exposed to users | herbelin | 2010-12-04 |
* | Fixing several bugs with links to notation in coqdoc, including bug #2445: | herbelin | 2010-12-04 |
* | Coqdoc patches from UPenn (thanks to C. Casinghino). This introduces the | msozeau | 2010-09-28 |
* | Minor fixes of 'make doc' | pboutill | 2010-09-28 |
* | Fixing bug #2389 (keyword "Declare Instance" unknown from "coqdoc -g") but | herbelin | 2010-09-19 |
* | Added test for bugs 2242, 2337, 2339 + remove the use of name "ambiguous" in | herbelin | 2010-09-18 |
* | Coqdep_boot : misc improvements | letouzey | 2010-09-17 |
* | Updated all headers for 8.3 and trunk | herbelin | 2010-07-24 |
* | Fix a bug found by S.Glondu. coq-db.el did not compile. | courtieu | 2010-07-23 |
* | Finish adding out-of-the-box support for camlp4 | letouzey | 2010-07-09 |
* | Remove dependency to Unix from module Profile | glondu | 2010-07-02 |
* | Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326) | glondu | 2010-06-03 |
* | Add (almost) compatibility with camlp4, without breaking support for camlp5 | letouzey | 2010-05-19 |
* | Remove compile-command pragmas for emacs | letouzey | 2010-05-19 |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | Fixing various coqdep bugs (#2118, #2242, #2274) | herbelin | 2010-04-10 |
* | Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing | herbelin | 2010-04-09 |
* | New model for user-driven translation of tokens in coqdoc | herbelin | 2010-04-06 |
* | Small things about coqdoc + fixing lettuple.v test (part of bug #2289) | herbelin | 2010-03-30 |
* | Removed hard-wiring of latin1 letters in coqdoc (see bug #2275) | herbelin | 2010-03-30 |
* | Small improvements around coqdoc (including fix for bug #2288) | herbelin | 2010-03-30 |
* | Fixed small bugs introduced in commit 12890 (bug #2286, that comes | herbelin | 2010-03-30 |
* | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |
* | Adding Function as keyword for coqdoc | thery | 2010-03-06 |
* | Coqdep_boot: when emultating ocamldep, avoid outputting empty answer | letouzey | 2010-03-04 |
* | Makefile: the .ml of .ml4 are now produced explicitely (in binary ast form) | letouzey | 2010-03-04 |
* | Fix previous commit | notin | 2010-01-28 |
* | Typo in previous commit | notin | 2010-01-28 |
* | Correction du bug #2219: application du patch envoyé par F. Garillot | notin | 2010-01-28 |
* | Report de la révision #12676 | notin | 2010-01-15 |
* | Fix "Existing Instance" to handle globality information and "Existing | msozeau | 2009-12-27 |
* | Fix make_exact_entry to allow applying [forall x, P x] hints directly, | msozeau | 2009-12-01 |
* | Correction du bug #2118 (Coqdep does not escape #) | notin | 2009-11-19 |
* | Suppression de l'appel à Lexing.new_line (qui n'existe pas dans les versions... | notin | 2009-11-12 |
* | Correction du bug #2183 | notin | 2009-11-10 |
* | Misc fixes. | msozeau | 2009-11-06 |
* | Correction du bug #2153 (-D n'est pas une option standard de install) | notin | 2009-11-05 |
* | Removed debugging stuff mistakenly introduced in r12426. | herbelin | 2009-11-03 |
* | Removed 'dest' from keyword highlighting. | gmelquio | 2009-10-30 |
* | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau | 2009-10-28 |
* | Add a new vernacular command for controling implicit generalization of | msozeau | 2009-10-27 |