| Commit message (Expand) | Author | Age |
|---|
| * | Names.mli: double declaration of mind_modpath |  letouzey | 2010-04-16 |
| * | Extraction: improvement of optimizations (kill_dummy, optim_fix) | letouzey | 2010-04-16 |
| * | Util: remove list_split_at which is a clone of list_chop | letouzey | 2010-04-16 |
| * | Extraction: ad-hoc identifier type with annotations for reductions | letouzey | 2010-04-16 |
| * | Compare_dec : a few better proofs (and extracted terms), some more Defined | letouzey | 2010-04-16 |
| * | Extraction: less _ in Haskell (typically for False_rect), less toplevel eta-e... | letouzey | 2010-04-16 |
| * | Removing redundant internal variants of apply tactic and simplification of ML... |  herbelin | 2010-04-14 |
| * | Remove only *.v.log files in clean of test-suite/Makefile |  glondu | 2010-04-13 |
| * | Look for csdp in $PATH at runtime, remove -csdpdir configure option | glondu | 2010-04-11 |
| * | Remove unused functions run_sdpa | glondu | 2010-04-11 |
| * | Recovering 8.2 behavior of "simple (e)apply" (and hence of "(e)auto"). | herbelin | 2010-04-11 |
| * | Run parallelized test-suite in "check" target of main Makefile | glondu | 2010-04-10 |
| * | Prettier test-suite/Makefile | glondu | 2010-04-10 |
| * | Optimized need for delimiters when disjoint scopes for strings and | herbelin | 2010-04-10 |
| * | Update .gitignore | glondu | 2010-04-10 |
| * | Use the Makefile in test-suite/check | glondu | 2010-04-10 |
| * | Makefile for the test-suite | glondu | 2010-04-10 |
| * | Fix typos in test-suite script | glondu | 2010-04-10 |
| * | Granting wish #2229 (InA_dec transparent) and Michael Day's coq-club | herbelin | 2010-04-10 |
| * | Test for bug #2231 (unexpected error when using let/if over an inductive | herbelin | 2010-04-10 |
| * | Partially fixed bug #2231 (an inductive parameter name was internally | herbelin | 2010-04-10 |
| * | Fixing various coqdep bugs (#2118, #2242, #2274) | herbelin | 2010-04-10 |
| * | Change definition of FSetList so that equality is Leibniz | glondu | 2010-04-09 |
| * | Add test-suite/lia.cache to .gitignore | glondu | 2010-04-09 |
| * | Fixing part 1 of bug #2242 (-I -as and -R -as were supported for | herbelin | 2010-04-09 |
| * | Granting wish #2249 (checking existing lemma name also when in a section). | herbelin | 2010-04-09 |
| * | Documenting the use of ##, %%, $$ in coqdoc. | herbelin | 2010-04-09 |
| * | Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing | herbelin | 2010-04-09 |
| * | Commit 12906 continued (forgotten file). | herbelin | 2010-04-07 |
| * | Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which | herbelin | 2010-04-07 |
| * | New model for user-driven translation of tokens in coqdoc | herbelin | 2010-04-06 |
| * | Improving compatibility between 8.2 and 8.3 | herbelin | 2010-04-05 |
| * | Fix configure script: natdynlink works without a hack on 10.6.3. |  msozeau | 2010-04-05 |
| * | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
| * | Changement de ide/proofs.ml en ide/ideproofs.ml pour éviter un conflit |  aspiwack | 2010-04-05 |
| * | Granting wish #2251 (forbidding rewriting a term reduced to an evar) | herbelin | 2010-04-05 |
| * | Tests for bug report #2244 (pattern-unification with abstraction over Meta's) | herbelin | 2010-04-05 |
| * | Partial fix to bug #2244 (ensure that pattern unification does not | herbelin | 2010-04-05 |
| * | Add documentation on the treatment of [if] and [let (x1, ... xn) := ..] | msozeau | 2010-03-31 |
| * | 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 |
| * | Manual qualification of Mfourier.Proof in micromega to avoid ocamldep using i... | letouzey | 2010-03-30 |
| * | Improving error messages in the presence of utf-8 characters | herbelin | 2010-03-30 |
| * | Several bug-fixes and improvements of coqdoc | herbelin | 2010-03-29 |
| * | Extended on-the-fly eta-expansion in coercion mechanism to sort-polymorphic | herbelin | 2010-03-28 |
| * | Fixing bug #2254 (inappropriate names of Zlt_gt_succ and Zlt_succ_gt) | herbelin | 2010-03-28 |
| * | Fixing bug #2279 (printing nested let-in was in exponential time) | herbelin | 2010-03-27 |
| * | Applied greenrd's patch to fix bug 2255 (injection failed to | herbelin | 2010-03-27 |
letouzey
herbelin
glondu
msozeau
aspiwack