aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
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
2009-06-01Prevent automatic inference of implicit arguments when the auto flag ismsozeau
2009-05-29Fix extract hyps to correctly discharge all hyps as described by keepmsozeau
2009-05-27Fix implicit args code so that declarations are added for allmsozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-04-24Backporting 12080 (fixing bug #2091 on bad rollback in the "where"herbelin
2009-04-10Fix premature optimisation in dependent induction: even variable args needmsozeau
2009-04-08Some dead code removal + cleanupsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:34:10 +0000