aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-04-03Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksletouzey
2011-03-17Goptions: repair Unset for int optionsletouzey
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-02-11Annotations at functor applications:letouzey
2011-02-10More comments and less doublons in some mlipboutill
2011-01-31A fine-grain control of inlining at functor application via priority levelsletouzey
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2011-01-11Fix some typosglondu
2010-10-31Minor code improvements around libobjectherbelin
2010-10-05Export definition of type implicits_list for contribs + fixed aherbelin
2010-10-04Fixing bugs in previous commits about implicit arguments:herbelin
2010-10-03Added multiple implicit arguments rules per name.herbelin
2010-10-03Dead code in impargs (afaics, no more need, since r11242, to mergeherbelin
2010-09-28Fix function applications without labels (OCaml warning 6)glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-18Fixing bugs #2347 (part 2) and #2388: error message printing was doneherbelin
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-08-27* library/Library: Reformulate a comment.regisgia
2010-08-27* library/Library: Document.regisgia
2010-08-27* lib/Flags: Replace dont_load_proofs by load_proofs since not loadingregisgia
2010-08-27* Improve documentation of LightenLibrary.regisgia
2010-08-27* (checker|kernel)/Safe_typing: New LightenLibrary.regisgia
2010-08-27* library/Library: Remove the use of the old-fashioned lighten_library.regisgia
2010-08-27* library/Library: Remove lighten_library definition.regisgia
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-07-23Some fine-tuning after removal of automatic imports of coercions in r13310herbelin
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-06-25Moved error when option does not exist into a warning (this allows toherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-22Protection against anomaly when loading a state with bad magic number.herbelin
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-06-03Added command "Locate Ltac qid".herbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-05-05Patch bug 2313.soubiran
2010-04-29"make source-doc" builds documentation of mli in html and pdf atpboutill
2010-04-29Various minor improvements of comments in mli for ocamldocletouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-27Added a new exception for already declared Schemes, vsiles
2010-04-16Util: remove list_split_at which is a clone of list_chopletouzey
2010-04-09Granting wish #2249 (checking existing lemma name also when in a section).herbelin
2010-03-29Several bug-fixes and improvements of coqdocherbelin
2010-02-12Simplify backtrackingvgross
2010-02-12Fixing closing of segments.vgross
2010-02-02Small fix on module inclusion.soubiran
2010-01-19Various bug fix on recent features of the module system:soubiran
2010-01-17Variant !F M for functor application that does not honor the Inline declarationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 07:19:28 +0000