| Age | Commit message (Expand) | Author |
|---|
| 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-14 | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin |
| 2010-04-13 | Remove only *.v.log files in clean of test-suite/Makefile | glondu |
| 2010-04-11 | 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-10 | 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-09 | 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-07 | Commit 12906 continued (forgotten file). | herbelin |
| 2010-04-07 | Granting wish #2251 thanks to commit 12900 solved bug 1416.v (which | herbelin |
| 2010-04-06 | New model for user-driven translation of tokens in coqdoc | herbelin |
| 2010-04-05 | 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-03-31 | Add documentation on the treatment of [if] and [let (x1, ... xn) := ..] | msozeau |
| 2010-03-30 | 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-29 | Several bug-fixes and improvements of coqdoc | herbelin |
| 2010-03-28 | 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-27 | 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-24 | Fixed bug #2260 (check of resolution of all evars in the declaration | herbelin |
