| Age | Commit message (Expand) | Author |
|---|
| 2010-05-04 | - Fixing bug #2308 about Lemma ... with | vsiles |
| 2010-05-04 | Correction of bug 2290 (removing stupid message) | jforest |
| 2010-05-04 | Correction of bug 2290 | jforest |
| 2010-05-03 | ocamldoc related fixes | pboutill |
| 2010-05-03 | Re-enable validation in "make check", run it in parallel with test-suite | glondu |
| 2010-05-02 | Fix discrimination of sorts which doesn't play well with cumulativity | msozeau |
| 2010-05-01 | Extraction: fix type_expunge_from_sign broken in last commit | letouzey |
| 2010-04-30 | Extraction: an experimental command to get rid of some cst/constructor arguments | letouzey |
| 2010-04-30 | Fail: a way to check that a command is refused without blocking a script | letouzey |
| 2010-04-29 | "make source-doc" builds documentation of mli in html and pdf at | pboutill |
| 2010-04-29 | After the approval of Bruno, here the patch for the checker. | soubiran |
| 2010-04-29 | Various minor improvements of comments in mli for ocamldoc | letouzey |
| 2010-04-29 | fixed bug #2224 (Error message in positivity check fixed) | vsiles |
| 2010-04-29 | Two forgotten $Id$ in last commit | letouzey |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-29 | Removed obsolete v7->v8 translation code (function check_same_type is | herbelin |
| 2010-04-29 | Move from ocamlweb to ocamdoc to generate mli documentation | pboutill |
| 2010-04-28 | Dont recompute the contents of the proof window when entering the | vgross |
| 2010-04-27 | 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-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 |
