| Age | Commit message (Expand) | Author |
|---|
| 2010-04-26 | Misc small fixes : warning, dep cycles, ocamlbuild... | letouzey |
| 2010-04-26 | Disable ideal-features tests by default | glondu |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2010-04-22 | Applying François Garillot's patch (#2261 in bug tracker) for extended | herbelin |
| 2010-04-22 | Ignore *.stamp files | herbelin |
| 2010-04-20 | Fixed bugs from commit 12954 on unification complexity | herbelin |
| 2010-04-20 | missing space in error message | vsiles |
| 2010-04-20 | Fixed bug #2999 (destruct was not refreshing universes of what it generalized *) | herbelin |
| 2010-04-20 | Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2 | herbelin |
| 2010-04-19 | Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2). | herbelin |
| 2010-04-19 | In function "substitution_prefixed_by" the prefix test on module path | soubiran |
| 2010-04-18 | Fixed some printing bugs. | herbelin |
| 2010-04-17 | A pass on the CHANGES file + credits for 8.3 (completing commit 12906 | herbelin |
| 2010-04-17 | Moved Case3.v from ideal features to success (it works since 8.2). | herbelin |
| 2010-04-17 | Solved a few problems of auto by bypassing the call to apply. | herbelin |
| 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 |
