| Age | Commit message (Expand) | Author |
|---|
| 2010-04-17 | Use nice "unfold" instead of ugly "change" to display calls to unfold hints | herbelin |
| 2010-04-16 | cf. 12945 | soubiran |
| 2010-04-16 | Extraction: cosmetics when using ocaml + Extract Inductive to symbols | letouzey |
| 2010-04-16 | Extraction: restore (temporarily?) a very limited form of linear letin reduction | letouzey |
| 2010-04-16 | Extraction: less eta in calls to global functions, better optimization phase | letouzey |
| 2010-04-16 | 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-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 |
