aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2010-05-10Backporting r13007 (evar_merge wrong and costly) to V8.3 and added test.herbelin
2010-05-10Fix: Pfedit.get_current_goal_context when no goal is focused.aspiwack
2010-05-10Removed an evar_merge in clenv_fchain which not only is incorrect butherbelin
2010-05-09Removed $Id$ introduced inadvertently in r13005 (no more $Id$ since r12972)herbelin
2010-05-09Added a few informations about file lineages (for the most part in kernel)herbelin
2010-05-09Update of credits filesherbelin
2010-05-07Fix bug #2315 : printing of defined evars in Coqide.aspiwack
2010-05-07Deux commentaires retirés de ocamldoc.aspiwack
2010-05-07better detection of nested recursion in Functionjforest
2010-05-07Correction of a bug pointed by P. Casteran.jforest
2010-05-07Trying to find a problem pointed by P. Casteranjforest
2010-05-06term matching in ltac was not coherent with match goal in presence of wildcar...jforest
2010-05-06Correction in Function documentationjforest
2010-05-05Patch bug 2313.soubiran
2010-05-05Pfedit.resume_proof doesn't implicitly Pfedit.suspend_proofpboutill
2010-05-04 - Fixing bug #2308 about Lemma ... withvsiles
2010-05-04Correction of bug 2290 (removing stupid message)jforest
2010-05-04Correction of bug 2290jforest
2010-05-03ocamldoc related fixespboutill
2010-05-03Re-enable validation in "make check", run it in parallel with test-suiteglondu
2010-05-02Fix discrimination of sorts which doesn't play well with cumulativitymsozeau
2010-05-01Extraction: fix type_expunge_from_sign broken in last commitletouzey
2010-04-30Extraction: an experimental command to get rid of some cst/constructor argumentsletouzey
2010-04-30Fail: a way to check that a command is refused without blocking a scriptletouzey
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29After the approval of Bruno, here the patch for the checker.soubiran
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29fixed bug #2224 (Error message in positivity check fixed)vsiles
2010-04-29Two forgotten $Id$ in last commitletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Removed obsolete v7->v8 translation code (function check_same_type isherbelin
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-28Dont recompute the contents of the proof window when entering thevgross
2010-04-27Fix bug #2245, incorrect handling of Context in sections inside modulemsozeau
2010-04-27 small detail about Scheme Equality vsiles
2010-04-27Added a new exception for already declared Schemes, vsiles
2010-04-26Misc small fixes : warning, dep cycles, ocamlbuild...letouzey
2010-04-26Disable ideal-features tests by defaultglondu
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-04-22Ignore *.stamp filesherbelin
2010-04-20Fixed bugs from commit 12954 on unification complexityherbelin
2010-04-20missing space in error messagevsiles
2010-04-20Fixed bug #2999 (destruct was not refreshing universes of what it generalized *)herbelin
2010-04-20Propagated fix to bug 2127 (Hint Rewrite badly globalized in modules) to 8.2herbelin
2010-04-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin
2010-04-19In function "substitution_prefixed_by" the prefix test on module path soubiran
2010-04-18Fixed some printing bugs.herbelin
2010-04-17A pass on the CHANGES file + credits for 8.3 (completing commit 12906herbelin
2010-04-17Moved Case3.v from ideal features to success (it works since 8.2).herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:02:41 +0000