| Commit message (Expand) | Author | Age |
* | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill | 2010-04-29 |
* | Dont recompute the contents of the proof window when entering the | vgross | 2010-04-28 |
* | Fix bug #2245, incorrect handling of Context in sections inside module | msozeau | 2010-04-27 |
* | small detail about Scheme Equality | vsiles | 2010-04-27 |
* | Added a new exception for already declared Schemes, | vsiles | 2010-04-27 |
* | Misc small fixes : warning, dep cycles, ocamlbuild... | letouzey | 2010-04-26 |
* | Disable ideal-features tests by default | glondu | 2010-04-26 |
* | 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-22 |
* | 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-20 |
* | 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-19 |
* | Fixed some printing bugs. | herbelin | 2010-04-18 |
* | 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-17 |
* | 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-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 |