aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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
2009-12-08Declaremods.ml: a useless function wrongly introduced in last commitletouzey
2009-12-07No more specific syntax "Include Self" for inclusion of partially-applied fun...letouzey
2009-12-03declaremods.ml <--- code factoringsoubiran
2009-12-01Continuing r12485-12486 (cleaning around name generation)herbelin
2009-11-18Now "Include Self <expr>" handles partially applied functors, cf for example ...soubiran
2009-11-18Module subtyping : allow many <: and module type declaration with <:letouzey
2009-11-16New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))letouzey
2009-11-16Include Self (Type) Foo: applying a (Type) Functor to the current contextletouzey
2009-11-11Fixed bug #2168 (closing a section may have as side-effect the erasureherbelin
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-30Undo 12432 which caused an exponential behavior at Requires. Compilation time...puech
2009-10-28Fix incorrect registration of objects in libtypes.ml when defining a module.puech
2009-10-28Same as commit 12430 but with the good version of the function iter_all_segmentsoubiran
2009-10-28From now SearchAbout requests search also inside INCLUDE libobject.soubiran
2009-10-26Local/Global revision 12418 continuedherbelin
2009-10-26New cleaning phase of the Local/Global option managementherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-23First debug... the renaming of librairies was not working and auto/dn were no...soubiran
2009-10-21This big commit addresses two problems:soubiran
2009-10-08Fixed a bug introduced in revision 12265.herbelin
2009-10-06Relaxed error severity when encountering unknown library objects or tacticgmelquio
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-17Fix typos in commentsglondu
2009-09-14Backtrack on the forced discharge of type class variables introducedmsozeau
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-27Correction bug 2140.soubiran
2009-08-14Ajout de la gestion de Local et Global pour les options (au sens deaspiwack
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-08-06Cleaning of Nametab continued + fixed a compilation bug in previous commit.herbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-02Improved parameterization of Coq:herbelin
2009-07-01Support for binding Coq root read-only in -R optionherbelin
2009-06-26propagation sur le trunk du commit 12101 soubiran
2009-06-26Add doc for [Print Opaque Dependencies] and a better explanation for themsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-23 00:19:37 +0000