aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* 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
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Backporting 12080 (fixing bug #2091 on bad rollback in the "where"Gravatar herbelin2009-04-24
* Fix premature optimisation in dependent induction: even variable args needGravatar msozeau2009-04-10
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* correction bug 2085Gravatar soubiran2009-04-06
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Bug 2050, commit v8.2 11923-11924 ---> trunkGravatar soubiran2009-02-13
* Correction bug coqdev Hermann lehener.Gravatar soubiran2009-02-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 02:10:37 +0000