aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
...
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Added a new exception for already declared Schemes, Gravatar vsiles2010-04-27
* Util: remove list_split_at which is a clone of list_chopGravatar letouzey2010-04-16
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* Simplify backtrackingGravatar vgross2010-02-12
* Fixing closing of segments.Gravatar vgross2010-02-12
* Small fix on module inclusion.Gravatar soubiran2010-02-02
* Various bug fix on recent features of the module system:Gravatar soubiran2010-01-19
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Declaremods.ml: a useless function wrongly introduced in last commitGravatar letouzey2009-12-08
* No more specific syntax "Include Self" for inclusion of partially-applied fun...Gravatar letouzey2009-12-07
* declaremods.ml <--- code factoringGravatar soubiran2009-12-03
* Continuing r12485-12486 (cleaning around name generation)Gravatar herbelin2009-12-01
* Now "Include Self <expr>" handles partially applied functors, cf for example ...Gravatar soubiran2009-11-18
* Module subtyping : allow many <: and module type declaration with <:Gravatar letouzey2009-11-18
* New syntax <+ for chains of Include (or Include Type) (or Include Self (Type))Gravatar letouzey2009-11-16
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* Fixed bug #2168 (closing a section may have as side-effect the erasureGravatar herbelin2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Undo 12432 which caused an exponential behavior at Requires. Compilation time...Gravatar puech2009-10-30
* Fix incorrect registration of objects in libtypes.ml when defining a module.Gravatar puech2009-10-28
* Same as commit 12430 but with the good version of the function iter_all_segmentGravatar soubiran2009-10-28
* From now SearchAbout requests search also inside INCLUDE libobject.Gravatar soubiran2009-10-28
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* First debug... the renaming of librairies was not working and auto/dn were no...Gravatar soubiran2009-10-23
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Fixed a bug introduced in revision 12265.Gravatar herbelin2009-10-08
* Relaxed error severity when encountering unknown library objects or tacticGravatar gmelquio2009-10-06
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix typos in commentsGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Correction bug 2140.Gravatar soubiran2009-08-27
* Ajout de la gestion de Local et Global pour les options (au sens deGravatar aspiwack2009-08-14
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* Cleaning of Nametab continued + fixed a compilation bug in previous commit.Gravatar herbelin2009-08-06
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Support for binding Coq root read-only in -R optionGravatar herbelin2009-07-01
* propagation sur le trunk du commit 12101 Gravatar soubiran2009-06-26
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
* Prevent automatic inference of implicit arguments when the auto flag isGravatar msozeau2009-06-01
* Fix extract hyps to correctly discharge all hyps as described by keepGravatar msozeau2009-05-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 21:38:10 +0000